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