proposition: Lemma eq_bool_ok : forall a1 a2, match eq_bool a1 a2 with true => a1 = a2 | false => ~a1 = a2 end.
proof: Proof. fix eq_bool_ok 1. intros [ | n] [ | m]; simpl. reflexivity. discriminate. discriminate. generalize (eq_bool_ok n m); case (eq_bool n m). intros; subst; reflexivity. intros n_diff_m Sn_eq_Sm; apply n_diff_m; injection Sn_eq_Sm; intro; assumption. Defined.
imports: Coq(Setoid Relations Arith FunInd)