proposition: Lemma find_clauses_Forall : forall (P : Annot.t watched_clause -> Prop) (i : literal) (cls : t), Forall P cls -> Forall_watch_map P (find_clauses i cls).
proof: Proof. unfold find_clauses. intros. destruct i. - destruct (IntMap.get' (id f) cls) eqn:EQ. + apply H in EQ; auto. destruct EQ ; auto. + apply IntMapForallEmpty. - destruct (IntMap.get' (id f) cls) eqn:EQ. + apply H in EQ; auto. destruct EQ ; auto. + apply IntMapForallEmpty. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause