1 2 3 4 5 6 7 8 9 10
Require Import BinPos. Definition P := (fun x : positive => x = xH). Goal forall (p q : positive), P q -> q = p -> P p. intros; congruence. Qed.