[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DNE(\<^bold>\<not>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>
[PROOF STEP]
oops