[STATEMENT]
lemma validD_L: \<open>\<tturnstile> \<phi> \<Longrightarrow> \<phi> \<in> Cn(A)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tturnstile> \<phi> \<Longrightarrow> \<phi> \<in> Cn A
[PROOF STEP]
using monotonicity_L valid_def infer_def
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> ?B \<Longrightarrow> Cn ?A \<subseteq> Cn ?B
\<tturnstile> ?\<phi> \<equiv> {} \<turnstile> ?\<phi>
?A \<turnstile> ?\<phi> \<equiv> ?\<phi> \<in> Cn ?A

goal (1 subgoal):
 1. \<tturnstile> \<phi> \<Longrightarrow> \<phi> \<in> Cn A
[PROOF STEP]
by fastforce