proposition: Lemma Forall_add_clause : forall (P: Annot.t watched_clause -> Prop) l i wc cls (WFW : wf cls) (PWC : P wc) (ALL : Forall P cls), Forall P (add_clause l i wc cls).
proof: Proof. intros. rewrite add_clause_eq by auto. unfold add_clause_old. intros. destruct(find_clauses_p (id_of_literal l) cls) as (ln,lp) eqn:EQ. assert (EQ':= EQ). apply WMap.Forall_find_clauses with (P:=P) in EQ; auto. destruct EQ as (LN & LP). apply wf_find_clauses_p in EQ'; auto. destruct EQ' as (WLN & WLP). destruct (is_positive_literal l). apply IntMapForallAdd;auto. destruct WFW;auto. split ; simpl ; auto. apply IntMapForallAdd;auto. apply IntMapForallAdd;auto. destruct WFW;auto. split ; simpl ; auto. apply IntMapForallAdd;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause