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