proposition: Lemma Forall_eval_literal_POS : forall l, Forall eval_literal (List.map POS l) <-> Forall eval_hformula l.
proof: Proof. induction l. - simpl. rewrite ! Forall_rew. tauto. - simpl. rewrite Forall_rew. symmetry. rewrite Forall_rew. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause