proposition: Lemma hold_eval_binop_neg : forall k f1 f2, hold k (eval_binop (fun x _ => x -> False) (fun x y => negb x) k f1 f2) <-> (hold k f1 -> False).
proof: Proof. destruct k ; simpl; intros. - tauto. - unfold is_true in *. rewrite negb_true_iff. destruct f1 ; intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause