proposition: Lemma T_Abs_inv: forall E x a t, E ⊢ Abs x a ∈ t -> exists t1 t2, ((x, t1) :: E) ⊢ a ∈ t2 /\ Fun 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); eauto. exists t1, t2; split. auto. apply subtype_trans with s; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)