proposition: Lemma bijective_transformation_bijective : forall u : E, bijective u -> Transformation.bijective (U (source u)) (U (target u)) (ev u).
proof: Proof. ir. unfold bijective in H; xe. unfold injective in H. unfold surjective in H0. xe. unfold axioms in H. unfold property in H. unfold Transformation.bijective in |- *; xe. Qed.
imports: Arith functions