proposition: Lemma wf_env_narrowing : forall V E F U X, wf_env (F ++ X ~ bind_sub V ++ E) -> wf_typ E U -> wf_env (F ++ X ~ bind_sub U ++ E).
proof: Proof. Proof with eauto using wf_typ_narrowing. induction F; intros U X Wf_env Wf; inversion Wf_env; subst; simpl_env in *... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure