\forall x,y:Z.
match eqZb x y with
[ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y].
+| false \Rightarrow x \neq y].
intros.
elim x.
elim y.
qed.
theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
-(x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
+(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
intros.
cut
match (eqZb x y) with
[ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y] \to P (eqZb x y).
+| false \Rightarrow x \neq y] \to P (eqZb x y).
apply Hcut.
apply eqZb_to_Prop.
elim (eqZb).