proposition: Lemma to_formula_correct : forall (f:BForm IsProp), eval_formula (eval_atom IsProp) (to_formula true IsProp f) -> eval_bformula IsProp f.
proof: Proof. apply (aux_to_formula_correct true IsProp). Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause