proposition: Lemma inv_Etyp_app : forall (P : Prop) (e : env) (u v T : term), Etyp e (App u v) T -> (forall V Ur : term, Etyp e u (Prod V Ur) -> Etyp e v V -> Econv T (subst v Ur) -> P) -> P.
proof: Proof. intros. apply Etyp_inversion with e (App u v) T; simpl in |- *; auto with coc ecoc core arith datatypes; intros. apply H0 with V Ur; auto with coc ecoc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types