二つの命題が相互依存になって、二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法になってしまった。 既知とする命題 既知の命題1: λx.Q ≡α λy.Q' ⇔ Q' ≡α [y/x]Q かつ [x≡y または y ∉ FV(Q)] 既知の命題2: R' ≡α R, λy.Q' ≡α λx.Q ⇒…