proposition: Lemma index_eq_indom : forall A B (M:map A B) k, index M k = (k \indom M).
proof: Proof. Proof using. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)