proposition: Lemma lookup_total_singleton_ne `{!Inhabited A} i j (x : A) : i ≠ j → ({[i := x]} : M A) !!! j = inhabitant.
proof: Proof. intros. by rewrite lookup_total_alt, lookup_singleton_ne. Qed.
imports: Coq(Permutation) stdpp(options)