proposition: Lemma eval_hformula_hlform : forall am f, eval_hformula (eval_prop am IsProp) (hlform f) <-> eval_hformula (eval_prop am IsProp) f.
proof: Proof. intros. apply eval_nform; auto. exact (fun _ => true). intro. rewrite <- eval_formula_lform. tauto. exact (fun _ => true). Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause