[STATEMENT]
lemma strand_subst_all_fv_subset:
  assumes "fv t \<subseteq> fv\<^sub>s\<^sub>t S" "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fv t \<subseteq> fv\<^sub>s\<^sub>t S
(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}

goal (1 subgoal):
 1. fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)
[PROOF STEP]
by (metis fv_strand_subst' Int_commute subst_apply_fv_subset)