proposition: Lemma refl_NF_Econv : forall t : term, normal t -> NF_Econv t t.
proof: Proof. simple induction t; auto with ecoc; intros. elim (normal_abs_inv t0 t1 H1); auto with ecoc. elim (normal_app_inv t0 t1 H1); intros. elim H3; auto with ecoc. elim (normal_prod_inv t0 t1 H1); auto with ecoc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm