[STATEMENT]
lemma min_one_proper_design: "proper_design \<V> \<B> \<or> proper_design \<V>' \<B>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_design \<V> \<B> \<or> proper_design \<V>' \<B>'
[PROOF STEP]
using blocks_nempty des1_is_proper des2_is_proper
[PROOF STATE]
proof (prove)
using this:
\<B> \<noteq> {#} \<or> \<B>' \<noteq> {#}
\<B> \<noteq> {#} \<Longrightarrow> proper_design \<V> \<B>
\<B>' \<noteq> {#} \<Longrightarrow> proper_design \<V>' \<B>'

goal (1 subgoal):
 1. proper_design \<V> \<B> \<or> proper_design \<V>' \<B>'
[PROOF STEP]
by (unfold_locales, blast)