proposition: Lemma wf_env_strengthening : forall x T E F, wf_env (F ++ x ~ bind_typ T ++ E) -> wf_env (F ++ E).
proof: Proof. Proof with eauto using wf_typ_strengthening. induction F; intros Wf_env; inversion Wf_env; subst; simpl_env in *... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure