proposition: Lemma NF_Econv_not_is_lam : forall M N : term, NF_Econv M N -> ~ is_lam M -> ~ is_lam N.
proof: Proof. intros M N H; inversion_clear H; auto; intros. unfold is_lam, not in |- *; intros (x, (x0, H3)); discriminate. elim H; unfold is_lam in |- *; split with T; split with M0; trivial. unfold is_lam, not in |- *; intros (x, (x0, H3)); discriminate. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm