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