proposition: Lemma wfb_correct : forall m, wfb m = true -> wf m.
proof: Proof. intros. unfold wfb in H. rewrite andb_true_iff in H. destruct H. constructor ; intros. - unfold wf_entry in H. destruct (IntMap.get' 0 m) ; try congruence. destruct p. rewrite andb_true_iff in H. destruct H. rewrite Bool.eqb_true_iff in H1. subst. apply is_FF_true in H. congruence. - unfold wf_entry in H0. destruct (IntMap.get' 1 m) ; try congruence. destruct p. rewrite andb_true_iff in H0. destruct H0. rewrite Bool.eqb_true_iff in H1. subst. apply is_TT_true in H0. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause