proposition: Lemma identity_axioms : forall a : E, axioms a a (Function.identity a).
proof: Proof. ir. unfold axioms in |- *; xd. ap Function.identity_axioms. ap Function.identity_domain. unfold sub in |- *; ir. assert (Function.axioms (Function.identity a)). ap Function.identity_axioms. pose (Function.range_ex H0 H). nin e; xd. rewrite Function.identity_domain in H1. rewrite Function.identity_ev in H2. rewrite <- H2; am. am. Qed.
imports: set_theory