proposition: Lemma T_App_inv: forall E a1 a2 t, E ⊢ App a1 a2 ∈ t -> exists t1 t2, E ⊢ a1 ∈ Fun t1 t2 /\ E ⊢ a2 ∈ t1 /\ t2 <: t.
proof: Proof. intros until t; intros TY; dependent induction TY. - exists t, t'; auto using subtype_refl. - edestruct IHTY as (t1 & t2 & P & Q & R); eauto. exists t1, t2; split. auto. split. auto. apply subtype_trans with s; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)