proposition: Lemma eq_nat_corr : forall n m:nat, eq_nat n m = true -> n = m.
proof: Proof. simple induction n; simple induction m; simpl in |- *; intros. trivial. inversion H0. inversion H0. rewrite (H n1 H1). trivial. Qed.
imports: CoRN.logic.CLogic Coq.Bool.Bool