proposition: Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.
proof: Proof. intros A B H. change ((fun _ => A) true = (fun _ => B) true). rewrite pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B). - reflexivity. - intros _; exact H. Qed.