proposition: Lemma sub_strengthening : forall x U E F S T, sub (F ++ x ~ bind_typ U ++ E) S T -> sub (F ++ E) S T.
proof: Proof. Proof with eauto using wf_typ_strengthening, wf_env_strengthening. intros x U E F S T SsubT. remember (F ++ x ~ bind_typ U ++ E) as E'. generalize dependent F. induction SsubT; intros F EQ; subst... Case "sub_trans_tvar". apply (sub_trans_tvar U0)... analyze_binds H... Case "sub_all". pick fresh X and apply sub_all... rewrite <- app_assoc. apply H0... Qed.
imports: Fsub.Fsub_LetSum_Lemmas