[STATEMENT]
lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw]  AnalLet_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
[PROOF STATE]
proof (state)
this:
?\<pi> \<bullet> PropApp \<equiv> PropApp
?\<pi> \<bullet> PropLam \<equiv> PropLam
?\<pi> \<bullet> PropLetBody \<equiv> PropLetBody
?\<pi> \<bullet> AnalLet \<equiv> AnalLet
?\<pi> \<bullet> PropLetHeap \<equiv> PropLetHeap
?\<pi> \<bullet> TransVar = TransVar
?\<pi> \<bullet> TransApp = TransApp
?\<pi> \<bullet> TransLam = TransLam
?\<pi> \<bullet> TransLet = TransLet

goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
note transform.eqvt[eqvt]
[PROOF STATE]
proof (state)
this:
?p \<bullet> transform ?a ?aa = transform (?p \<bullet> ?a) (?p \<bullet> ?aa)

goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
apply (rule supp_fun_app_eqvt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (transform a)
[PROOF STEP]
apply (rule eqvtI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<bullet> transform a \<equiv> transform a
[PROOF STEP]
apply perm_simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. transform a \<equiv> transform a
[PROOF STEP]
apply (rule reflexive)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
supp (transform a e) \<subseteq> supp e

goal:
No subgoals!
[PROOF STEP]
qed