proposition: Lemma surjective_rewrite : forall u : E, axioms u -> surjective u = (forall x : E, inc x (U (target u)) -> ex (fun y : E => (inc y (U (source u)) & ev u y = x))).
proof: Proof. ir. ap iff_eq; ir. unfold surjective in H0; xe. unfold Transformation.surjective in H2; xe. au. unfold surjective in |- *; xe. unfold Transformation.surjective in |- *; xe. Qed.
imports: Arith functions