定理証明手習い (57) 見えない

142ページの

ここで関数wtを使いましょう。

から

:
ここでも、いまと同じステップが使えそうですね。
:
これで3回めになりますが、同じステップですかね？
:
次の2つのフォーカスで関数wtを使いましょう。
:
まず、associate-+の公理を使います。
:

を経由して

common-addends-<を使って(wt (cdr x))をキャンセルできますからね。

まで、何やってるのかわかんね感がぱない
言われたとおりにやればそうなるんだけど

(wt (cdr x))をキャンセルできる形に持っていける見込みがあって変形していってるんだろうか
その見通しってやつが見えない

ここは「洞察」ないのかな