proposition: Lemma eval_clause_or : forall env l, eval_clause env (map POS l) <-> eval_or env l.
proof: Proof. induction l;simpl. - tauto. - rewrite IHl. unfold eval_lit. simpl. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause