proposition: Lemma hcons_bprover_correct : forall n (f:BForm.HBForm) am, hcons_bprover am (empty_thy_prover ) n f = true -> BForm.eval_hbformula (eval_prop am) f.
proof: Proof. intros n f am. intros. apply BForm.to_hformula_correct with (has_bool := has_bool am). - apply has_bool_correct. - unfold hcons_bprover in H. apply hcons_prover_correct with (eval_atom := eval_prop am IsProp) in H. rewrite eval_hformula_hlform in H. auto. apply is_dec_correct. apply empty_thy. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause