+
+theorem bool_to_decidable_eq:
+ \forall b1,b2:bool. decidable (b1=b2).
+ intros.
+ unfold decidable.
+ elim b1.
+ elim b2.
+ left. reflexivity.
+ right. exact not_eq_true_false.
+ elim b2.
+ right. unfold Not. intro.
+ apply not_eq_true_false.
+ symmetry. exact H.
+ left. reflexivity.
+qed.
+
+theorem P_x_to_P_x_to_eq:
+ \forall A:Set. \forall P: A \to bool.
+ \forall x:A. \forall p1,p2:P x = true. p1 = p2.
+ intros.
+ apply eq_to_eq_to_eq_p_q.
+ exact bool_to_decidable_eq.
+qed.