Create monadic version of insert

[gallais]

Insert should be allowed to fail (e.g. if we don't want to override existing values):
For that to work, we need update with the type:

update : (TotalStrictOrder ltR, Monad m) =>
         (k : key) -> ({k1 : key} -> k = k1 -> Maybe (val k1) -> m (val k1)) ->
	 ExtendLT ltR l (Lift k) -> ExtendLT ltR (Lift k) u ->
         Tree ltR val l u n -> m (MayFit ltR val l u n)