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