proposition: Lemma Econv_sort_prod : forall (s : sort) (t u : term), ~ Econv (Srt s) (Prod t u).
proof: Proof. red in |- *; intros. elim Econv_church_rosser with (Srt s) (Prod t u); auto with ecoc coc core arith sets. do 2 intro. elim Ered_Enormal with (Srt s) x; auto with ecoc coc core arith sets. intro. apply Ered_prod_prod with t u (Srt s); auto with ecoc coc core arith sets; intros. discriminate H2. red in |- *; red in |- *; intros. inversion_clear H1. Qed.
imports: Termes Conv