proposition: Lemma hformula_eqb_refl (f1: HFormula) : hformula_eqb f1 f1 = true.
proof: Proof. unfold hformula_eqb. destruct f1 ; simpl in *. unfold xhformula_eqb. unfold HCons.eq_hc. simpl. rewrite! andb_true_iff. split_and. lia. apply eqb_reflx. apply formula_eqb_refl. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Morphisms Cdcl.Lib Cdcl.Syntax