@Kha I implemented the following approach: - Error if user tries to revert `auxDecl`. - Clear any `auxDecl` that depends on variables being reverted by the user.
#lang lean4
simp