[STATEMENT]
lemma fold_graph_Or\<^sub>n:
  "finite \<Phi> \<Longrightarrow> fold_graph Or_ltln False_ltln \<Phi> (Or\<^sub>n \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph Or_ltln false\<^sub>n \<Phi> (Or\<^sub>n \<Phi>)
[PROOF STEP]
unfolding Or\<^sub>n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph Or_ltln false\<^sub>n \<Phi> (SOME \<phi>. fold_graph Or_ltln false\<^sub>n \<Phi> \<phi>)
[PROOF STEP]
by (rule someI2_ex[OF finite_imp_fold_graph])