proposition: Lemma unit_or_correct : forall f, eval_hformula f <-> eval_literal_list (unit_or f).
proof: Proof. unfold unit_or. intros. destruct (elt f) eqn:F; simpl; unfold eval_hformula; try tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause