proposition: Lemma inv_typ_prod : forall (P : Prop) e T (U s : term), typ e (Prod T U) s -> (forall s1 s2, typ e T (Srt s1) -> typ (T :: e) U (Srt s2) -> conv (Srt s2) s -> P) -> P.
proof: Proof. intros. apply typ_inversion with e (Prod T U) s; simpl in |- *; auto with coc core arith datatypes; intros. apply H0 with s1 s2; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList