[STATEMENT]
lemma StartBallot_HInv3_p:   
  "\<lbrakk> StartBallot s s' p; HInv3_L s' p q d \<rbrakk> 
          \<Longrightarrow> HInv3_R s' p q d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>StartBallot s s' p; HInv3_L s' p q d\<rbrakk> \<Longrightarrow> HInv3_R s' p q d
[PROOF STEP]
by(auto simp add: StartBallot_def dest: InitPhase_HInv3_p)