>「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ掲載されていない
>一階述語理論としてのZFCの形式化自体は特にそれほど難しい作業ではない

ならさっさとやれ　やってから御託並べろ