tactics for subsingletons

Stream: general

[Chris Hughes]

Is there a version of exact that doesn't care if two subsingleton terms are not defeq. Same question for rw. If not, I might have a go at writing one.