proposition: Lemma injective_rewrite : forall u : E, axioms u -> injective u = (forall x y : E, inc x (U (source u)) -> inc y (U (source u)) -> ev u x = ev u y -> x = y).
proof: Proof. ir. ap iff_eq; ir. unfold injective in H0. xe. unfold Transformation.injective in H4. xe. au. unfold injective in |- *; xe. unfold Transformation.injective in |- *; xe. Qed.
imports: Arith functions