「関数プログラミング入門」でも結構最初の方に紹介されてたテクニックだが
両辺のf xをyと置いてより一般的な命題にしてyに関する帰納法という手もあるな
実質は式変形してモナド則の証明の形に持ってくるのと同じことやってるわけだけど