こういうのってCoq ?とかで機械的に証明できないのかしら？
腹落ちする理解はできないないけど論理的には合ってるみたいな。