[
    [ BeginEnv "signature"
    , Label "example_cons"
    , BeginEnv "math"
    , Command "cons"
    , InvisibleBraceL
    , Variable "y"
    , InvisibleBraceR
    , InvisibleBraceL
    , Variable "X"
    , InvisibleBraceR
    , EndEnv "math"
    , Word "is"
    , Word "a"
    , Word "set"
    , Symbol "."
    , EndEnv "signature"
    ]
,
    [ BeginEnv "signature"
    , Label "example_pair"
    , BeginEnv "math"
    , ParenL
    , Variable "x"
    , Symbol ","
    , Variable "y"
    , ParenR
    , EndEnv "math"
    , Word "is"
    , Word "a"
    , Word "set"
    , Symbol "."
    , EndEnv "signature"
    ]
,
    [ BeginEnv "axiom"
    , Label "cons"
    , BeginEnv "math"
    , Variable "x"
    , Command "in"
    , Command "cons"
    , InvisibleBraceL
    , Variable "y"
    , InvisibleBraceR
    , InvisibleBraceL
    , Variable "X"
    , InvisibleBraceR
    , EndEnv "math"
    , Word "iff"
    , BeginEnv "math"
    , Variable "x"
    , Symbol "="
    , Variable "y"
    , EndEnv "math"
    , Word "or"
    , BeginEnv "math"
    , Variable "x"
    , Command "in"
    , Variable "X"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "axiom"
    ]
,
    [ BeginEnv "definition"
    , Label "times"
    , BeginEnv "math"
    , Variable "A"
    , Command "times"
    , Variable "B"
    , Symbol "="
    , VisibleBraceL
    , ParenL
    , Variable "a"
    , Symbol ","
    , Variable "b"
    , ParenR
    , Command "mid"
    , Variable "a"
    , Command "in"
    , Variable "A"
    , Symbol ","
    , Variable "b"
    , Command "in"
    , Variable "B"
    , VisibleBraceR
    , EndEnv "math"
    , Symbol "."
    , EndEnv "definition"
    ]
,
    [ BeginEnv "definition"
    , Label "unit"
    , BeginEnv "math"
    , Command "unit"
    , Symbol "="
    , VisibleBraceL
    , Command "emptyset"
    , VisibleBraceR
    , EndEnv "math"
    , Symbol "."
    , EndEnv "definition"
    ]
,
    [ BeginEnv "proposition"
    , Label "pair_emptyset_in_times_unit"
    , BeginEnv "math"
    , ParenL
    , Command "emptyset"
    , Symbol ","
    , Command "emptyset"
    , ParenR
    , Command "in"
    , Command "unit"
    , Command "times"
    , Command "unit"
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "definition"
    , Label "suc"
    , BeginEnv "math"
    , Command "suc"
    , InvisibleBraceL
    , Variable "a"
    , InvisibleBraceR
    , Symbol "="
    , VisibleBraceL
    , Variable "y"
    , Command "mid"
    , Command "exists"
    , Variable "x"
    , Command "in"
    , Variable "a"
    , Symbol "."
    , Variable "y"
    , Symbol "="
    , VisibleBraceL
    , Variable "x"
    , VisibleBraceR
    , VisibleBraceR
    , EndEnv "math"
    , Symbol "."
    , EndEnv "definition"
    ]
,
    [ BeginEnv "proposition"
    , Label "times_replacement_test"
    , BeginEnv "math"
    , Variable "A"
    , Command "times"
    , Variable "B"
    , Symbol "="
    , VisibleBraceL
    , ParenL
    , Variable "a"
    , Symbol ","
    , Variable "b"
    , ParenR
    , Command "mid"
    , Variable "a"
    , Command "in"
    , Variable "A"
    , Symbol ","
    , Variable "b"
    , Command "in"
    , Variable "B"
    , VisibleBraceR
    , EndEnv "math"
    , Symbol "."
    , EndEnv "proposition"
    ]
,
    [ BeginEnv "proof"
    , Word "follows"
    , Word "by"
    , Ref
        ( "times" :| [] )
    , Symbol "."
    , EndEnv "proof"
    ]
]