proposition: Lemma inv_Etyp_prod : forall (P : Prop) (e : env) (T U s : term), Etyp e (Prod T U) s -> (forall s1 s2 : sort, Etyp e T (Srt s1) -> Etyp (T :: e) U (Srt s2) -> Econv (Srt s2) s -> P) -> P.
proof: Proof. intros. apply Etyp_inversion with e (Prod T U) s; simpl in |- *; auto with coc ecoc core arith datatypes; intros. apply H0 with s1 s2; auto with coc ecoc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types