proposition: Lemma trans_NF_Econv_NF_Econv : forall M N : term, NF_Econv M N -> forall P : term, NF_Econv N P -> NF_Econv M P.
proof: Proof. simple induction 1; auto with ecoc; intros. inversion H5; auto with ecoc. inversion H4; auto with ecoc. inversion H4; auto with ecoc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm