proposition: Lemma eqb_true (A:Type) (x y:A) (eqb:A->A->bool) (eqb_spec : forall x y, if eqb x y then x = y else x <> y) (P:eqb x y = true) : x = y.
proof: Proof. generalize (eqb_spec x y); intro H. destruct (eqb x y). assumption. discriminate P. Qed.