proposition: Lemma normal_normal_app : forall M N : term, normal M -> normal N -> ~ is_lam M -> normal (App M N).
proof: Proof. intros; unfold normal, not in |- *; intros. generalize H H1; clear H H1; inversion_clear H2. intros. apply H1. unfold is_lam in |- *; split with T; split with M0; trivial. intros H1; elim H1 with N1; auto with coc. elim H0 with N2; auto with coc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm