[STATEMENT]
lemma lift_subst_ML:
 "lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v)
[PROOF STEP]
apply(induct \<sigma> v rule:subst_ML.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> nm. lift k (subst\<^sub>M\<^sub>L \<sigma> (C\<^sub>M\<^sub>L nm)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (C\<^sub>M\<^sub>L nm))
 2. \<And>\<sigma> X. lift k (subst\<^sub>M\<^sub>L \<sigma> (V\<^sub>M\<^sub>L X)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (V\<^sub>M\<^sub>L X))
 3. \<And>\<sigma> v vs. \<lbrakk>lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v); \<And>x. x \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> x) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k x)\<rbrakk> \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (A\<^sub>M\<^sub>L v vs)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (A\<^sub>M\<^sub>L v vs))
 4. \<And>\<sigma> v. lift k (subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## \<sigma>) v) = subst\<^sub>M\<^sub>L (lift k \<circ> V\<^sub>M\<^sub>L 0 ## \<sigma>) (lift k v) \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (Lam\<^sub>M\<^sub>L v)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (Lam\<^sub>M\<^sub>L v))
 5. \<And>\<sigma> nm vs. (\<And>x. x \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> x) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k x)) \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (C\<^sub>U nm vs)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (C\<^sub>U nm vs))
 6. \<And>\<sigma> x vs. (\<And>xa. xa \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> xa) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k xa)) \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (V\<^sub>U x vs)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (V\<^sub>U x vs))
 7. \<And>\<sigma> v vs n. \<lbrakk>lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v); \<And>x. x \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> x) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k x)\<rbrakk> \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (Clo v vs n)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (Clo v vs n))
 8. \<And>\<sigma> u v. \<lbrakk>lift k (subst\<^sub>M\<^sub>L \<sigma> u) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k u); lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v)\<rbrakk> \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (apply u v)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (apply u v))
[PROOF STEP]
apply(simp_all add: o_assoc lift_o_shift del:apply_cons_ML)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> v. lift k (subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## \<sigma>) v) = subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## (lift k \<circ> \<sigma>)) (lift k v) \<Longrightarrow> subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## (lift k \<circ> \<sigma>)) (lift k v) = subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## (\<lambda>a. lift k (\<sigma> a))) (lift k v)
[PROOF STEP]
apply(simp add:o_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done