[STATEMENT]
lemma pos_literal_in_imp_true_cls[intro]: "Pos A \<in># C \<Longrightarrow> A \<in> I \<Longrightarrow> I \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pos A \<in># C; A \<in> I\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
using true_cls_def
[PROOF STATE]
proof (prove)
using this:
(?I \<Turnstile> ?C) = (\<exists>L\<in>#?C. ?I \<Turnstile>l L)

goal (1 subgoal):
 1. \<lbrakk>Pos A \<in># C; A \<in> I\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
by blast