proposition: Lemma PropExt_and_PropFunExt_imp_PredExt : PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality.
proof: Proof. intros Ext FunExt A P Q Equiv. apply FunExt. intros x. now apply Ext. Qed.