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