proposition: Lemma hold_eval_binop_or : forall k f1 f2, hold k (eval_binop or orb k f1 f2) <-> (hold k f1 \/ hold k f2).
proof: Proof. destruct k ; simpl; intros. - tauto. - unfold is_true. rewrite orb_true_iff. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause