proposition: Lemma Ered1_normal_NF_Econv : forall T T' : term, Ered1 T T' -> normal T -> NF_Econv T T'.
proof: Proof. simple induction 1; intros. elim H0 with (subst N M); auto with coc. elim (normal_abs_inv T0 M H0); intros. apply trans_NF_Econv_NF_Econv with (Abs (Srt prop) M); auto with ecoc. elim (normal_abs_inv M N H2); eauto with ecoc. elim (normal_abs_inv N M H2); eauto 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