Hola Bruno.
Yo uso en general "->" en vez de "/\" para cosas del tipos A /\ B -> C; esto es: A -> B -> C.
Recomiendo usar la flecha (->), aunque el /\ debería funcionar ya que lógicamente es equivalente, pero puedo comprobar que en Coq, al menos en este caso, es como decís al hacer inducción en la hipóteis con isomorfo.
Saludos, Carlos