[STATEMENT]
lemma subst_idemE: "subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
assume "subst_idem \<sigma>"
[PROOF STATE]
proof (state)
this:
subst_idem \<sigma>

goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
hence "\<And>v. fv (\<sigma> v) \<inter> subst_domain \<sigma> = {}"
[PROOF STATE]
proof (prove)
using this:
subst_idem \<sigma>

goal (1 subgoal):
 1. \<And>v. fv (\<sigma> v) \<inter> subst_domain \<sigma> = {}
[PROOF STEP]
unfolding subst_idem_def subst_compose_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<sigma> x \<cdot> \<sigma>) = \<sigma>

goal (1 subgoal):
 1. \<And>v. fv (\<sigma> v) \<inter> subst_domain \<sigma> = {}
[PROOF STEP]
by (metis trm_subst_disj)
[PROOF STATE]
proof (state)
this:
fv (\<sigma> ?v) \<inter> subst_domain \<sigma> = {}

goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fv (\<sigma> ?v) \<inter> subst_domain \<sigma> = {}

goal (1 subgoal):
 1. subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
unfolding range_vars_alt_def
[PROOF STATE]
proof (prove)
using this:
fv (\<sigma> ?v) \<inter> subst_domain \<sigma> = {}

goal (1 subgoal):
 1. subst_domain \<sigma> \<inter> fv\<^sub>s\<^sub>e\<^sub>t (subst_range \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_domain \<sigma> \<inter> range_vars \<sigma> = {}

goal:
No subgoals!
[PROOF STEP]
qed