refactor: back rfl
tactic primarily via apply_rfl
#3718
Merged
rfl
tactic primarily via apply_rfl
#3718