proposition: Lemma eval_literal_list_POS : forall l , eval_literal_list (List.map POS l) <-> (eval_or_list' eval_hformula l).
proof: Proof. induction l; simpl. - tauto. - intros. unfold eval_hformula at 1. rewrite IHl. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause