proposition: Lemma lookup_delete `{EqDec k} i j m : lookup i (delete j m) = if eq_dec i j then None else lookup i m.
proof: Proof. induction m; simpl. - destruct (eq_dec i j) eqn:Heqe1. + destruct (eq_dec j k0) eqn:Heqe2; auto. simpl; subst. now rewrite Heqe2. + destruct (eq_dec j k0) eqn:Heqe2; simpl; auto. * subst. now rewrite Heqe1. * now destruct (eq_dec i k0). - now destruct (eq_dec i j). Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib