proposition: Lemma mor_create : forall o m c i s u, property o m c i-> mor (create o m c i s) u = inc u m.
proof: Proof. ir. set (k:= create o m c i s). assert (lem0 : axioms k). uf k; ap create_axioms; am. assert (lem1 : forall u, mor k u = is_mor k u). ir. ap iff_eq; ir. lu. uhg; ee; am. rw lem1. uf k; rw is_mor_create; tv. Qed.
imports: Arith universe