proposition: Lemma wf_add_clause : forall l id cl cls (WF: wf cls), wf (add_clause l id cl cls).
proof: Proof. intros. rewrite add_clause_eq by auto. assert (WF':= WF). unfold wf in WF. unfold wf. destruct WF as (WFM & WF). split. apply wf_map_add_clause_old; auto. unfold IntMapForall in *; intros. unfold add_clause_old in H. destruct (find_clauses_p (id_of_literal l) cls) eqn:EQ. apply wf_find_clauses_p in EQ; auto. destruct EQ as(WF1 & WF2). destruct (is_positive_literal l); rewrite gsspec in H ; auto; destruct (eqs k (id_of_literal l)); eauto. - inv H; simpl ; split ; auto with wf. - inv H; simpl ; split ; auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause