proposition: Lemma wf_typ_strengthening : forall E F x U T, wf_typ (F ++ x ~ bind_typ U ++ E) T -> wf_typ (F ++ E) T.
proof: Proof. Proof with simpl_env; eauto. intros E F x U T H. remember (F ++ x ~ bind_typ U ++ E) as G. generalize dependent F. induction H; intros F Heq; subst... Case "wf_typ_var". analyze_binds H... Case "wf_typ_all". pick fresh Y and apply wf_typ_all... rewrite <- app_assoc. apply H1... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure