左右が逆だって

rw h は等式的法則 h （hは等式的法則のラベル）を使ってターゲット内の項を別な項で置き換える。

• rw ←h とすると、a=>b 方向のリライトをする。矢印が逆！
• rw h とすると、a<=b 方向のリライトをする。

まったく！