[ BlockDefn
    ( Location
        { locFile = "test/examples/proofdefinefunction.tex"
        , locLine = 3
        , locColumn = 1
        }
    ) Nothing
    ( Marker "apply" )
    ( DefnOp
        ( SymbolPattern
            ( MixfixItem
                ( TokenCons
                    ( Command "apply" )
                    ( TokenCons InvisibleBraceL
                        ( HoleCons
                            ( TokenCons InvisibleBraceR
                                ( TokenCons InvisibleBraceL
                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
                                )
                            )
                        )
                    )
                )
                ( Marker "apply" ) NonAssoc
            )
            [ NamedVar "f"
            , NamedVar "x"
            ]
        )
        ( ExprVar
            ( NamedVar "x" )
        )
    )
, BlockDefn
    ( Location
        { locFile = "test/examples/proofdefinefunction.tex"
        , locLine = 8
        , locColumn = 1
        }
    ) Nothing
    ( Marker "dom" )
    ( DefnOp
        ( SymbolPattern
            ( MixfixItem
                ( TokenCons
                    ( Command "dom" )
                    ( TokenCons InvisibleBraceL
                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
                    )
                )
                ( Marker "dom" ) NonAssoc
            )
            [ NamedVar "f" ]
        )
        ( ExprVar
            ( NamedVar "f" )
        )
    )
, BlockDefn
    ( Location
        { locFile = "test/examples/proofdefinefunction.tex"
        , locLine = 13
        , locColumn = 1
        }
    ) Nothing
    ( Marker "rightunique" )
    ( Defn []
        ( DefnAdj Nothing
            ( NamedVar "f" )
            ( Adj
                ( Location
                    { locFile = "test/examples/proofdefinefunction.tex"
                    , locLine = 14
                    , locColumn = 12
                    }
                )
                ( LexicalItem
                    ( TokenCons
                        ( Word "right-unique" ) End
                    )
                    ( Marker "rightunique" )
                ) []
            )
        )
        ( StmtFormula
            { formula = FormulaChain
                ( ChainBase
                    ( ExprVar
                        ( NamedVar "f" ) :| []
                    ) Positive
                    ( Relation
                        ( Location
                            { locFile = "test/examples/proofdefinefunction.tex"
                            , locLine = 14
                            , locColumn = 31
                            }
                        )
                        ( RelationSymbol
                            ( Symbol "=" )
                            ( ParameterArity 0 )
                            ( Marker "eq" )
                        ) []
                    )
                    ( ExprVar
                        ( NamedVar "f" ) :| []
                    )
                )
            }
        )
    )
, BlockDefn
    ( Location
        { locFile = "test/examples/proofdefinefunction.tex"
        , locLine = 18
        , locColumn = 1
        }
    ) Nothing
    ( Marker "relation" )
    ( Defn []
        ( DefnNoun
            ( NamedVar "f" )
            ( Noun
                ( Location
                    { locFile = "test/examples/proofdefinefunction.tex"
                    , locLine = 19
                    , locColumn = 14
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "relation" ) End
                        , pl = TokenCons
                            ( Word "relations" ) End
                        }
                    )
                    ( Marker "relation" )
                ) []
            )
        )
        ( StmtFormula
            { formula = FormulaChain
                ( ChainBase
                    ( ExprVar
                        ( NamedVar "f" ) :| []
                    ) Positive
                    ( Relation
                        ( Location
                            { locFile = "test/examples/proofdefinefunction.tex"
                            , locLine = 19
                            , locColumn = 29
                            }
                        )
                        ( RelationSymbol
                            ( Symbol "=" )
                            ( ParameterArity 0 )
                            ( Marker "eq" )
                        ) []
                    )
                    ( ExprVar
                        ( NamedVar "f" ) :| []
                    )
                )
            }
        )
    )
, BlockClaim Proposition
    ( Location
        { locFile = "test/examples/proofdefinefunction.tex"
        , locLine = 22
        , locColumn = 1
        }
    ) Nothing
    ( Marker "definefunctiontest" )
    ( Claim []
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/proofdefinefunction.tex"
                    , locLine = 23
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtFormula
                { formula = FormulaChain
                    ( ChainBase
                        ( ExprVar
                            ( NamedVar "x" ) :| []
                        ) Positive
                        ( Relation
                            ( Location
                                { locFile = "test/examples/proofdefinefunction.tex"
                                , locLine = 23
                                , locColumn = 10
                                }
                            )
                            ( RelationSymbol
                                ( Command "in" )
                                ( ParameterArity 0 )
                                ( Marker "elem" )
                            ) []
                        )
                        ( ExprVar
                            ( NamedVar "y" ) :| []
                        )
                    )
                }
            , stmt2 = StmtFormula
                { formula = FormulaChain
                    ( ChainBase
                        ( ExprVar
                            ( NamedVar "x" ) :| []
                        ) Positive
                        ( Relation
                            ( Location
                                { locFile = "test/examples/proofdefinefunction.tex"
                                , locLine = 23
                                , locColumn = 25
                                }
                            )
                            ( RelationSymbol
                                ( Command "in" )
                                ( ParameterArity 0 )
                                ( Marker "elem" )
                            ) []
                        )
                        ( ExprVar
                            ( NamedVar "y" ) :| []
                        )
                    )
                }
            }
        )
    )
, BlockProof
    ( Location
        { locFile = "test/examples/proofdefinefunction.tex"
        , locLine = 25
        , locColumn = 1
        }
    )
    ( DefineFunction
        ( Location
            { locFile = "test/examples/proofdefinefunction.tex"
            , locLine = 26
            , locColumn = 5
            }
        )
        ( NamedVar "f" )
        ( NamedVar "z" )
        ( ExprVar
            ( NamedVar "z" )
        )
        ( NamedVar "z" )
        ( ExprVar
            ( NamedVar "x" )
        ) ( Qed Nothing JustificationEmpty )
    )
    ( Location
        { locFile = "test/examples/proofdefinefunction.tex"
        , locLine = 27
        , locColumn = 1
        }
    )
]