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