proposition: Lemma wf_find_clauses_p : forall i cls ln lp (WF : WMap.wf cls) (FD : find_clauses_p i cls = (ln, lp)), wf_map ln /\ wf_map lp.
proof: Proof. intros. unfold find_clauses_p in FD. destruct (IntMap.get' i cls) eqn:EQ. - subst. apply WF in EQ; auto. - inv FD. split; apply wf_map_empty. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause