proposition: Lemma sub_weakening : forall E F G S T, sub (G ++ E) S T -> wf_env (G ++ F ++ E) -> sub (G ++ F ++ E) S T.
proof: Proof. Proof with simpl_env; auto using wf_typ_weakening. intros E F G S T Sub Ok. remember (G ++ E) as H. generalize dependent G. induction Sub; intros G Ok EQ; subst... Case "sub_trans_tvar". apply (sub_trans_tvar U)... Case "sub_all". pick fresh Y and apply sub_all... rewrite <- app_assoc. apply H0... Qed.
imports: Fsub.Fsub_LetSum_Lemmas