proposition: Lemma identity_axioms : forall a : E, axioms a -> mor_axioms (identity a).
proof: Proof. ir. cx. uf mor_axioms; ee; clst. am. am. ap identity_strong_axioms. ir. rw ev_identity. rw ev_identity. am. lu. lu. Qed.
imports: universe