[
    [ BeginEnv "proposition"
    , Label "trivial"
    , BeginEnv "math"
    , Variable "x"
    , Symbol "="
    , Variable "x"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "proposition"
    , Label "irrelevant"
    , BeginEnv "math"
    , Variable "z"
    , Symbol "="
    , Variable "z"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "proposition"
    , Label "alsotrivial"
    , BeginEnv "math"
    , Variable "y"
    , Symbol "="
    , Variable "y"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "proof"
    , BeginEnv "align*"
    , Variable "y"
    , Symbol "&="
    , Variable "y"
    , Symbol "&="
    , Variable "y"
    , BeginEnv "text"
    , Word "by"
    , Ref
        ( "trivial" :| [] )
    , EndEnv "text"
    , EndEnv "align*"
    , EndEnv "proof"
    ]
,
    [ BeginEnv "proposition"
    , Label "trivial_biconditionals"
    , BeginEnv "math"
    , Variable "y"
    , Symbol "="
    , Variable "y"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "proof"
    , BeginEnv "align*"
    , Variable "y"
    , Symbol "="
    , Variable "y"
    , Symbol "&"
    , Command "iff"
    , Command "top"
    , Symbol "&"
    , Command "iff"
    , Variable "y"
    , Symbol "="
    , Variable "y"
    , BeginEnv "text"
    , Word "by"
    , Ref
        ( "trivial" :| [] )
    , EndEnv "text"
    , EndEnv "align*"
    , EndEnv "proof"
    ]
,
    [ BeginEnv "proposition"
    , Label "bounded_calc"
    , Word "for"
    , Word "all"
    , BeginEnv "math"
    , Variable "x"
    , Command "in"
    , Variable "A"
    , EndEnv "math"
    , Word "we"
    , Word "have"
    , BeginEnv "math"
    , Variable "x"
    , Symbol "="
    , Variable "x"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "proof"
    , Word "for"
    , Word "all"
    , BeginEnv "math"
    , Variable "x"
    , Command "in"
    , Variable "A"
    , EndEnv "math"
    , Word "we"
    , Word "have"
    , BeginEnv "align*"
    , Variable "x"
    , Symbol "&="
    , Variable "x"
    , EndEnv "align*"
    , EndEnv "proof"
    ]
,
    [ BeginEnv "proposition"
    , Label "bounded_calc_such_that"
    , Word "for"
    , Word "all"
    , BeginEnv "math"
    , Variable "x"
    , Command "in"
    , Variable "A"
    , EndEnv "math"
    , Word "such"
    , Word "that"
    , BeginEnv "math"
    , Variable "x"
    , Symbol "="
    , Variable "x"
    , EndEnv "math"
    , Word "we"
    , Word "have"
    , BeginEnv "math"
    , Variable "x"
    , Symbol "="
    , Variable "x"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "proof"
    , Word "for"
    , Word "all"
    , BeginEnv "math"
    , Variable "x"
    , Command "in"
    , Variable "A"
    , EndEnv "math"
    , Word "such"
    , Word "that"
    , BeginEnv "math"
    , Variable "x"
    , Symbol "="
    , Variable "x"
    , EndEnv "math"
    , Symbol ","
    , Word "we"
    , Word "have"
    , BeginEnv "align*"
    , Variable "x"
    , Symbol "&="
    , Variable "x"
    , EndEnv "align*"
    , EndEnv "proof"
    ]
]