[ 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"
]