proposition: Lemma eq_nat_spec: forall a b, reflect (a=b) (eq_nat_bool a b).
proof: Proof. induction a; intros [|b]; simpl; try constructor; auto. case (IHa ( b)); intros H; subst; constructor; auto. Qed.
imports: ATBR(Common) Coq(Equality Program Sumbool Peano)