proposition: Lemma delete_comm `{EqDec k} i j m : delete i (delete j m) = delete j (delete i m).
proof: Proof. generalize dependent j. generalize dependent i. induction m; simpl; intros; auto. destruct (eq_dec i k0) eqn:Heqe1; auto; simpl. - destruct (eq_dec j k0) eqn:Heqe2; auto; simpl. now rewrite Heqe1. - destruct (eq_dec j k0) eqn:Heqe2; auto; simpl. rewrite Heqe1. now rewrite IHm. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib