[STATEMENT]
lemma ssubst_sopen_distrib[rule_format]:
  "\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t 
   = {n \<rightarrow> [[x \<rightarrow> t']s, [x \<rightarrow> t']p]} [x \<rightarrow> t'] t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
have
    "(\<forall>n s p t'. lc t' 
       \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t']s, [x \<rightarrow> t']p]} [x \<rightarrow> t'] t)
    &(\<forall>n s p t'. lc t' 
       \<longrightarrow> ssubst_option x t' (sopen_option n s p u) 
           = sopen_option n ([x \<rightarrow> t']s) ([x \<rightarrow> t']p) (ssubst_option x t' u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t) \<and> (\<forall>n s p t'. lc t' \<longrightarrow> ssubst_option x t' (sopen_option n s p u) = sopen_option n ([x \<rightarrow> t'] s) ([x \<rightarrow> t'] p) (ssubst_option x t' u))
[PROOF STEP]
by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split)
[PROOF STATE]
proof (state)
this:
(\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t) \<and> (\<forall>n s p t'. lc t' \<longrightarrow> ssubst_option x t' (sopen_option n s p u) = sopen_option n ([x \<rightarrow> t'] s) ([x \<rightarrow> t'] p) (ssubst_option x t' u))

goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
from conjunct1[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t

goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t

goal:
No subgoals!
[PROOF STEP]
qed