proposition: Lemma indom_of_indom_update_at_indom : forall A `{Inhab B} (m:map A B) (i j:A) (v:B), j \indom (m[i:=v]) -> i \indom m -> j \indom m.
proof: Proof. Proof using. introv IB H F. rewrite~ indom_update_eq in H. destruct~ H. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)