proposition: Lemma inv_typ_app : forall (P : Prop) e u v T, typ e (App u v) T -> (forall V Ur : term, typ e u (Prod V Ur) -> typ e v V -> conv T (subst v Ur) -> P) -> P.
proof: Proof. intros. apply typ_inversion with e (App u v) T; simpl in |- *; auto with coc core arith datatypes; intros. apply H0 with V Ur; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList