proposition: Lemma read_update : forall A `{Inhab B} (m:map A B) (i j:A) (v:B), (m[i:=v])[j] = (If i = j then v else m[j]).
proof: Proof. Proof using. intros. rewrite update_impl_eq. simpl. unfold read_impl. case_if~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)