proposition: Lemma umorphism_create_extensionality : forall a b f a1 b1 f1, a = a1 -> b = b1 -> (forall x, inc x (U a) -> inc (f x) (U b)) -> (forall x, inc x (U a) -> f x = f1 x) -> Umorphism.create a b f = Umorphism.create a1 b1 f1.
proof: Proof. ir. assert (Umorphism.property a b f). uhg; ee. uhg; ee. am. assert (Umorphism.property a1 b1 f1). wr H. wr H0. uhg. uhg. ir. wr H2. au. am. ap Umorphism.extens. ap create_strong_axioms. am. ap create_strong_axioms. am. rw Umorphism.source_create. rww Umorphism.source_create. rww Umorphism.target_create. rww Umorphism.target_create. ir. rwi Umorphism.source_create H5. rwi Umorphism.source_create H6. rww ev_create. rww ev_create. au. Qed.
imports: Arith ordinal nat_trans