[STATEMENT]
theorem HInit_Inv2b: "HInit s \<longrightarrow> Inv2b s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInit s \<longrightarrow> Inv2b s
[PROOF STEP]
by (auto simp add: HInit_def Init_def Inv2b_def 
                   Inv2b_inner_def InitDB_def)