proposition: Lemma create_extensionality : forall (a b : E) (f g : E1), a = b -> (forall x : E, inc x a -> inc x b -> f x = g x) -> create a f = create b g.
proof: Proof. ir. assert (axioms (create a f)). ap create_axioms. assert (axioms (create b g)). ap create_axioms. ap function_extensionality; au. unfold defined in |- *; ir. xd. rewrite create_domain. rewrite <- H. rewrite create_domain in H4. am. unfold defined in |- *. ir; xd. rewrite create_domain. rewrite create_domain in H4. rewrite H. am. ir. assert (inc x a). unfold defined in H3. xd. rewrite create_domain in H4; am. repeat rewrite create_V_rewrite. ap H0. am. rewrite <- H. am. rewrite <- H. am. am. Qed.
imports: set_theory