proposition: Lemma eval_annot_hyp : forall m l (HL: has_literal m l), eval_annot eval_literal m (annot_hyp l).
proof: Proof. unfold annot_hyp. unfold eval_annot, annot_of_literal. simpl. intros. apply eval_pset_singleton in H. rewrite <- literal_eq; auto. apply has_form_of_literal; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause