Commit 2022-04-22 01:34 bb9d1c50
View on Github →chore(*): remove subst when not necessary (#13453)
Where possible, this replaces subst with obtain rfl (which is equivalent to have and then subst, golfing a line).
This also tidies some non-terminal simps.