proposition: Lemma remove_clause_eq : forall l clause_id cls, wf cls -> remove_watched_id l clause_id cls= remove_watched_id_old l clause_id cls.
proof: Proof. intros. apply IntMap.ptrie_extensional with (o:= None). - apply wf_map_remove_watched_id; auto. apply H. - apply wf_remove_watched_id_old; auto. - unfold remove_watched_id, remove_watched_id_old. unfold is_positive_literal, id_of_literal, form_of_literal. intros. destruct l. destruct (eq_dec k (id f)). { subst. rewrite IntMap.gis' with (opt:= None) by apply H. unfold find_clauses_p. destruct (IntMap.get' (id f) 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' (id f) 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. } destruct (eq_dec k (id f)). { subst. rewrite IntMap.gis' with (opt:= None) by apply H. unfold find_clauses_p. destruct (IntMap.get' (id f) 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' (id f) 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