proposition: Lemma is_hFF_true : forall g, is_hFF g = true -> g = hFF.
proof: Proof. unfold is_hFF. destruct g ; simpl. intros. unfold hFF. repeat rewrite andb_true_iff in H. destruct H as ((H1 & H2) & H3). rewrite eqb_true_iff in H2. subst. apply is_FF_true in H3. subst. assert (id0 = 0) by lia. subst. reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause