[STATEMENT]
lemma beforex_beforex\<^sub>0_eq:
 "P,C,M \<rhd> xt / I,d \<equiv> \<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 P C M d I xt xt\<^sub>0 xt\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,C,M \<rhd> xt / I,d \<equiv> \<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 P C M d I xt xt\<^sub>0 xt\<^sub>1
[PROOF STEP]
using beforex_def
[PROOF STATE]
proof (prove)
using this:
(?P,?C,?M \<rhd> ?xt / ?I,?d) = (\<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 ?P ?C ?M ?d ?I ?xt xt\<^sub>0 xt\<^sub>1)

goal (1 subgoal):
 1. P,C,M \<rhd> xt / I,d \<equiv> \<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 P C M d I xt xt\<^sub>0 xt\<^sub>1
[PROOF STEP]
by auto