[STATEMENT]
lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True
[PROOF STEP]
by (induction t) auto