前回: 構造の定義 - kururu_goedel’s diary 二項関係 論理式の定義 次回予告どおりに関係とその充足について。BoundedFormulaの定義を再掲。 /-- `BoundedFormula α n` is the type of formulas with free variables indexed by `α` and up to `n` additiona…