[STATEMENT]
lemma rule_sub_remark_8:
    assumes "\<And>v.[\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]"
        and "[\<^bold>\<box>(\<^bold>\<A>\<phi>) in v]"
    shows "[\<^bold>\<box>(\<phi>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<box>\<phi> in v]
[PROOF STEP]
apply (insert assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]; [\<^bold>\<box>\<^bold>\<A>\<phi> in v]\<rbrakk> \<Longrightarrow> [\<^bold>\<box>\<phi> in v]
[PROOF STEP]
apply PLM_autosubst
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]; [\<^bold>\<box>\<^bold>\<A>\<phi> in v]\<rbrakk> \<Longrightarrow> \<forall>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]
 2. \<lbrakk>\<And>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]; [\<^bold>\<box>\<^bold>\<A>\<phi> in v]\<rbrakk> \<Longrightarrow> [\<^bold>\<box>\<^bold>\<A>\<phi> in v]
[PROOF STEP]
by auto