proposition: Theorem PropExt_and_PropFunExt_iff_PredExt : PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality.
proof: Proof. firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt. Qed.