[ BeginEnv "proposition"
, Label "formula_test_forall"
, BeginEnv "math"
, Command "forall"
, Variable "x"
, Symbol ","
, Variable "y"
, Symbol "."
, Variable "x"
, Symbol "="
, Variable "x"
, Command "land"
, Variable "y"
, Symbol "="
, Variable "y"
, EndEnv "math"
, Symbol "."
, EndEnv "proposition"
, BeginEnv "proposition"
, Label "formula_test_exists"
, BeginEnv "math"
, Command "exists"
, Variable "x"
, Symbol ","
, Variable "y"
, Symbol "."
, Variable "x"
, Symbol "="
, Variable "y"
, EndEnv "math"
, Symbol "."
, EndEnv "proposition"
, BeginEnv "proposition"
, Label "formula_test_not_exists"
, BeginEnv "math"
, Command "exists"
, Variable "x"
, Symbol ","
, Variable "y"
, Symbol "."
, Variable "x"
, Symbol "="
, Variable "y"
, EndEnv "math"
, Word "if"
, Word "and"
, Word "only"
, Word "if"
, Word "not"
, BeginEnv "math"
, Command "exists"
, Variable "x"
, Symbol "."
, Variable "x"
, Command "neq"
, Variable "x"
, EndEnv "math"
, Symbol "."
, EndEnv "proposition"
]