proposition: Lemma indom_update_eq : forall A `{Inhab B} (m:map A B) (i j:A) (v:B), j \indom (m[i:=v]) = (j = i \/ j \indom m).
proof: Proof. Proof using. intros. rewrite dom_update. rew_set. extens*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)