proposition: Lemma Ered1_normal_normal : forall M N : term, Ered1 M N -> normal M -> normal N.
proof: Proof. simple induction 1; intros. elim H0 with (subst N0 M0); auto with coc. elim (normal_abs_inv T M0 H0); auto with ecoc. elim (normal_abs_inv M0 N0 H2); auto with ecoc. elim (normal_abs_inv N0 M0 H2); auto with ecoc. elim (normal_app_inv M1 M2 H2); intros. elim H4; eauto with ecoc. elim (normal_app_inv M1 M2 H2); intros. elim H4; eauto with ecoc. elim (normal_prod_inv M1 M2 H2); auto with ecoc. elim (normal_prod_inv M1 M2 H2); auto with ecoc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm