proposition: Lemma create_extens : forall (x x' y y' : E) (f g : E1), x = x' -> y = y' -> (forall a : E, inc a (U x) -> f a = g a) -> create x y f = create x' y' g.
proof: Proof. ir. wr H; wr H0. uf create. ap uneq. ap create_extensionality. tv. ir. au. Qed.
imports: Arith functions