proposition: Lemma Forall_find_clauses : forall P i cl ln lp (EC : Forall P cl) (FD : find_clauses_p i cl = (ln, lp)), IntMapForall P ln /\ IntMapForall P lp.
proof: Proof. unfold find_clauses_p. intros. destruct (IntMap.get' i cl) eqn:EQ. - destruct p. inv FD. apply EC in EQ; auto. - inv FD. split ; apply IntMapForallEmpty. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause