proposition: Lemma wf_env_subst_tb : forall Q Z P E F, wf_env (F ++ Z ~ bind_sub Q ++ E) -> wf_typ E P -> wf_env (map (subst_tb Z P) F ++ E).
proof: Proof. Proof with eauto 6 using wf_typ_subst_tb. induction F; intros Wf_env WP; simpl_env; inversion Wf_env; simpl_env in *; simpl subst_tb... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure