-
-theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
-(n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)).
-intros.
-cut
-(match (eqb n m) with
-[ true \Rightarrow n = m
-| false \Rightarrow n \neq m] \to (P (eqb n m))).
-apply Hcut.apply eqb_to_Prop.
-elim (eqb n m).
-apply ((H H2)).
-apply ((H1 H2)).
-qed.
-