proposition: Lemma cnf_plus_impli : forall hf l r (EQ : elt hf = LIMPL l r), eval_watched_clause {| watch1 := NEG r; watch2 := POS hf; unwatched := nil |}.
proof: Proof. unfold eval_watched_clause. simpl. intros. left. rewrite EQ. rewrite eval_formula_rew. rewrite <- eval_impl_list_eq. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause