proposition: Lemma isomap_isotrans_rw : forall x y, are_isomorphic x y -> isomap x y = Function.create x (isotrans x y).
proof: Proof. ir. uf isotrans. rw create_rw. tv. cp (isomap_bij H). uh H0; ee. uh H0; ee. rw H3; tv. cp (isomap_bij H). uh H0; ee. uh H0; ee. am. Qed.
imports: set_theory