proposition: Lemma eval_annot_lit : forall m l (HL: has_form m l), eval_annot eval_literal m (annot_lit l).
proof: Proof. unfold annot_lit. intros. apply eval_annot_hyp;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause