proposition: Lemma eq_expr_corr : forall e e':expr, eq_expr e e' = true -> e = e'.
proof: Proof. simple induction e; simple induction e'; simpl in |- *; intros; try inversion H3; try inversion H2; try inversion H1; try inversion H0; try inversion H. cut (v = v0). intro. rewrite H0; auto. apply eq_nat_corr; assumption. cut (z = z0). intro. rewrite H0; auto. apply eq_int_corr; assumption. clear H1 H2. elim (andb_prop _ _ H3); intros. cut (e0 = e2). cut (e1 = e3). intros. rewrite H4; rewrite H6. auto. apply H0. assumption. apply H. assumption. clear H1 H2. elim (andb_prop _ _ H3); intros. cut (e0 = e2). cut (e1 = e3). intros. rewrite H4; rewrite H6. auto. apply H0. assumption. apply H. assumption. clear H1 H2. elim (andb_prop _ _ H3); intros. cut (e0 = e2). cut (e1 = e3). intros. rewrite H4; rewrite H6. auto. apply H0. assumption. apply H. assumption. clear H0. elim (andb_prop _ _ H1); intros. cut (u = u0). cut (e0 = e1). intros. rewrite H4. rewrite H5. auto. apply H. assumption. apply eq_nat_corr. assumption. clear H1 H2. elim (andb_prop _ _ H3). intros. elim (andb_prop _ _ H2); intros. cut (b = b0). cut (e0 = e2). cut (e1 = e3). intros. rewrite H7. rewrite H8. rewrite H9. auto. auto. auto. apply eq_nat_corr. assumption. clear H0. elim (andb_prop _ _ H1); intros. cut (p = p0). cut (e0 = e1). intros. rewrite H4. rewrite H5. auto. auto. apply eq_nat_corr. assumption. Qed.
imports: CoRN.logic.CLogic Coq.Bool.Bool