proposition: Lemma insert_delete `{EqDec k} i x m : insert i x (delete i m) ≈ insert i x m.
proof: Proof. induction m; simpl; intros; auto. destruct (eq_dec i k0) eqn:Heqe. - subst. rewrite IHm; clear IHm. now rewrite lookup_insert. - simpl. rewrite Heqe; simpl. now rewrite IHm. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib