proposition: Lemma normal_app_inv : forall M N : term, normal (App M N) -> normal M /\ normal N /\ ~ is_lam M.
proof: Proof. unfold normal in |- *; intuition. apply H with (App u N); auto with coc. apply H with (App M u); auto with coc. generalize H0; clear H0; unfold is_lam in |- *; intros (T, (x0, H0)). rewrite H0 in H; apply H with (subst N x0); auto with coc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm