proposition: Lemma hformula_eq_dec (f1 f2: HFormula) : {f1 = f2} + {f1 <> f2}.
proof: Proof. destruct (hformula_eqb f1 f2) eqn:HF. apply hformula_eqb_true in HF. left ; auto. right. intro. subst. rewrite hformula_eqb_refl in HF. discriminate. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Morphisms Cdcl.Lib Cdcl.Syntax