proposition: Lemma eval_clause_POS : forall env p cl, (forall l : t, In l cl -> l = POS p) -> eval_clause env cl -> env p.
proof: Proof. induction cl; simpl. - tauto. - intros. unfold eval_lit in H0. rewrite (H _ (or_introl eq_refl)) in *. simpl in H0. destruct H0;auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause