proposition: Lemma conv_sort_prod : forall s t u, ~ conv (Srt s) (Prod t u).
proof: Proof. red in |- *; intros. elim church_rosser with (Srt s) (Prod t u); auto with coc core arith sets. do 2 intro. elim red_normal with (Srt s) x; auto with coc core arith sets. intro. apply red_prod_prod with t u (Srt s); auto with coc core arith sets; intros. discriminate H2. red in |- *; red in |- *; intros. inversion_clear H1. Qed.
imports: Termes