本でもマニュアルでも大変分かりずらく解説されてある unfold を使ってみます。関数を使うという意味で unfold は apply となんだか良く似ています。 unfold はゴールの中の関数名を定義で置き換えます。 apply は前提の関数型 A->B の B がゴールにマッチす…