proposition: Lemma wf_find_clauses : forall i cls (WF : wf cls), wf_watch_map (find_clauses i cls).
proof: Proof. intros. unfold find_clauses. destruct i. - destruct (IntMap.get' (id f) cls) eqn:EQ. + apply WF in EQ; auto. tauto. + apply wf_map_empty. - destruct (IntMap.get' (id f) cls) eqn:EQ. + apply WF in EQ; auto. tauto. + 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