proposition: Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality.
proof: Proof. intros Ext A B Equiv. change A with ((fun _ => A) I). now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B). Qed.