proposition: Lemma eval_literal_list_classic : forall m l (HF : Forall (has_literal m) l) (EV: eval_literal_list l) (C : check_classic l = true), eval_or l.
proof: Proof. induction l; simpl ; auto. intros. destruct_in_hyp C ISC; try congruence. inv HF. destruct a; simpl in *. - intuition. - apply eval_formula_dec in H1 ; auto. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause