proposition: Lemma hcons_prover_correct : forall thy (THY: Thy thy) n f , hcons_prover thy n f = true -> eval_hformula f.
proof: Proof. unfold hcons_prover. intros. unfold prover_bformula in H. destruct (prover_formula thy false (hcons_form f) n f) eqn:EQ; try congruence. destruct r. destruct p. apply prover_formula_correct in EQ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause