blob: 8f5488a602146f33d9e80a7196a8ca5badfef730 [file] [edit]
Try this: simp only [↓f_eq]