proposition: Lemma add_clause_eq : forall l clause_id cl cls, wf cls -> add_clause l clause_id cl cls= add_clause_old l clause_id cl cls.
proof: Proof. intros. apply IntMap.ptrie_extensional with (o:= None). - apply wf_map_add_clause; auto. apply H. - apply wf_map_add_clause_old; auto. apply H. - unfold add_clause, add_clause_old. unfold is_positive_literal, id_of_literal, form_of_literal. destruct l. intros. destruct (eq_dec k f.(id)). { subst. rewrite IntMap.gis' with (opt:= None) by apply H. unfold find_clauses_p. destruct (IntMap.get' f.(id) cls) eqn:G. destruct p. rewrite IntMap.gss' with (opt := None) by apply H. reflexivity. rewrite IntMap.gss' with (opt := None) by apply H. reflexivity. } { unfold find_clauses_p. rewrite IntMap.gio' with (opt:= None); auto. destruct (IntMap.get' f.(id) cls) eqn:G. destruct p. rewrite IntMap.gso' with (opt := None);auto. apply H. rewrite IntMap.gso' with (opt := None);auto. apply H. apply H. } intro. destruct (eq_dec k f.(id)). { subst. rewrite IntMap.gis' with (opt:= None) by apply H. unfold find_clauses_p. destruct (IntMap.get' f.(id) cls) eqn:G. destruct p. rewrite IntMap.gss' with (opt := None) by apply H. reflexivity. rewrite IntMap.gss' with (opt := None) by apply H. reflexivity. } { unfold find_clauses_p. rewrite IntMap.gio' with (opt:= None); auto. destruct (IntMap.get' f.(id) cls) eqn:G. destruct p. rewrite IntMap.gso' with (opt := None);auto. apply H. rewrite IntMap.gso' with (opt := None);auto. apply H. apply H. } Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause