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