proposition: Lemma prop_ext_em_degen : prop_extensionality -> excluded_middle -> prop_degeneracy.
proof: Proof. intros Ext EM A. destruct (EM A). - left; apply (Ext A True); split; [ exact (fun _ => I) | exact (fun _ => H) ]. - right; apply (Ext A False); split; [ exact H | apply False_ind ]. Qed.