ベック／シュバレー条件〈Beck-Chevalley condition〉の一般的な記述（例えば、nLab項目）は抽象的で何を言ってるのか分かりにくいです。ベック／シュバレー条件の具体例として、述語論理における限量子と代入〈substitution | 置換〉の交換可能性があります…