proposition: Lemma my_read_write : forall (m:map int val) (i j:int) (v:val), m[i := v][j] = (If i = j then v else m[j]).
proof: Proof. Proof using. intros. rewrite read_update. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet LibContainer LibMap)