proposition: Lemma normal_prod_inv : forall T U : term, normal (Prod T U) -> normal T /\ normal U.
proof: Proof. unfold normal in |- *; intuition. apply H with (Prod u U); auto with coc. apply H with (Prod T u); auto with coc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm