[STATEMENT]
lemma "\<lfloor>(\<lambda>X. \<^bold>\<diamond>\<^bold>\<exists>X) \<^bold>\<down>(P::\<up>\<langle>\<up>\<zero>\<rangle>) \<^bold>\<rightarrow> \<^bold>\<diamond>((\<lambda>X. \<^bold>\<exists>X) \<^bold>\<down>P)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<diamond>\<lparr>mexistsB P w\<rparr> \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsB P) w)\<rfloor>
[PROOF STEP]
nitpick[card 't=1, card i=2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<diamond>\<lparr>mexistsB P w\<rparr> \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsB P) w)\<rfloor>
[PROOF STEP]
oops \<comment> \<open>countersatisfiable\<close>