proposition: Lemma delete_idem `{EqDec k} i m : delete i (delete i m) = delete i m.
proof: Proof. induction m; simpl; auto. destruct (eq_dec i k0) eqn:Heqe; auto; simpl. rewrite Heqe. now rewrite IHm. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib