proposition: Lemma not_is_lam_Ered1 : forall M N : term, Ered1 M N -> normal M -> ~ is_lam M -> ~ is_lam N.
proof: Proof. simple induction 1; intros. elim H0 with (subst N0 M0); auto with coc. elim H1; unfold is_lam in |- *; split with T; split with M0; trivial. elim H3; unfold is_lam in |- *; split with M0; split with N0; trivial. elim H3; unfold is_lam in |- *; split with N0; split with M0; trivial. unfold not in |- *; unfold is_lam in |- *; intros (x, (x0, H4)); discriminate. unfold not in |- *; unfold is_lam in |- *; intros (x, (x0, H4)); discriminate. unfold not in |- *; unfold is_lam in |- *; intros (x, (x0, H4)); discriminate. unfold not in |- *; unfold is_lam in |- *; intros (x, (x0, H4)); discriminate. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm