proposition: Lemma prop_ext_retract_A_A_imp_A : prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A).
proof: Proof. intros Ext A a. rewrite (prop_ext_A_eq_A_imp_A Ext A a). exists (fun x:A => x) (fun x:A => x). reflexivity. Qed.
imports: PropExtensionalityFacts