proposition: Lemma create_recovers : forall f : E, axioms f -> create (domain f) (fun x : E => V x f) = f.
proof: Proof. ir. ap function_extensionality. ap create_axioms. am. ir. unfold defined in H0. xd. unfold defined in |- *. xd. rewrite create_domain in H1. am. ir. unfold defined in H0. xd. unfold defined in |- *; xd. ap create_axioms. rewrite create_domain. am. ir. unfold defined in H0; xd. rewrite create_domain in H1. ap create_V_apply; au. Qed.
imports: set_theory