proposition: Lemma normal_normal_abs : forall T M : term, normal T -> normal M -> normal (Abs T M).
proof: Proof. intros; unfold normal, not in |- *; intros. inversion_clear H1. elim H with M'; auto with coc. elim H0 with M'; auto with coc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm