proposition: Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality.
proof: Proof. intros H A B [Hab Hba]. destruct (H A); destruct (H B). - rewrite H1; exact H0. - absurd B. + rewrite H1; exact (fun H => H). + apply Hab; rewrite H0; exact I. - absurd A. + rewrite H0; exact (fun H => H). + apply Hba; rewrite H1; exact I. - rewrite H1; exact H0. Qed.