proposition: Lemma wf_map_add_clause_old : forall l id cl cls (WF: wf_map cls), wf_map (add_clause_old l id cl cls).
proof: Proof. unfold add_clause_old. intros. destruct (find_clauses_p (id_of_literal l) cls). destruct (is_positive_literal l); auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause