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