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