[ BlockDefn
    ( SourcePos
        { sourceName = "test/examples/proofdefinefunction.tex"
        , sourceLine = Pos 3
        , sourceColumn = Pos 1
        }
    )
    ( Marker "apply" )
    ( DefnOp
        [ Just
            ( Command "apply" )
        , Just InvisibleBraceL
        , Nothing
        , Just InvisibleBraceR
        , Just InvisibleBraceL
        , Nothing
        , Just InvisibleBraceR
        ]
        [ NamedVar "f"
        , NamedVar "x"
        ]
        ( TermVar
            ( NamedVar "x" )
        )
    )
, BlockDefn
    ( SourcePos
        { sourceName = "test/examples/proofdefinefunction.tex"
        , sourceLine = Pos 8
        , sourceColumn = Pos 1
        }
    )
    ( Marker "dom" )
    ( DefnOp
        [ Just
            ( Command "dom" )
        , Just InvisibleBraceL
        , Nothing
        , Just InvisibleBraceR
        ]
        [ NamedVar "f" ]
        ( TermVar
            ( NamedVar "f" )
        )
    )
, BlockDefn
    ( SourcePos
        { sourceName = "test/examples/proofdefinefunction.tex"
        , sourceLine = Pos 13
        , sourceColumn = Pos 1
        }
    )
    ( Marker "rightunique" )
    ( DefnPredicate []
        ( PredicateAdj
            [ Just
                ( Word "right-unique" )
            ]
        )
        ( NamedVar "f" :| [] )
        ( TermSymbol
            ( SymbolPredicate
                ( PredicateRelation
                    ( Symbol "=" )
                )
            )
            [ TermVar
                ( NamedVar "f" )
            , TermVar
                ( NamedVar "f" )
            ]
        )
    )
, BlockDefn
    ( SourcePos
        { sourceName = "test/examples/proofdefinefunction.tex"
        , sourceLine = Pos 18
        , sourceColumn = Pos 1
        }
    )
    ( Marker "relation" )
    ( DefnPredicate []
        ( PredicateNoun
            ( SgPl
                { sg =
                    [ Just
                        ( Word "relation" )
                    ]
                , pl =
                    [ Just
                        ( Word "relations" )
                    ]
                }
            )
        )
        ( NamedVar "f" :| [] )
        ( TermSymbol
            ( SymbolPredicate
                ( PredicateRelation
                    ( Symbol "=" )
                )
            )
            [ TermVar
                ( NamedVar "f" )
            , TermVar
                ( NamedVar "f" )
            ]
        )
    )
, BlockLemma
    ( SourcePos
        { sourceName = "test/examples/proofdefinefunction.tex"
        , sourceLine = Pos 22
        , sourceColumn = Pos 1
        }
    )
    ( Marker "definefunctiontest" )
    ( Lemma []
        ( Connected Implication
            ( TermSymbol
                ( SymbolPredicate
                    ( PredicateRelation
                        ( Command "in" )
                    )
                )
                [ TermVar
                    ( NamedVar "x" )
                , TermVar
                    ( NamedVar "y" )
                ]
            )
            ( TermSymbol
                ( SymbolPredicate
                    ( PredicateRelation
                        ( Command "in" )
                    )
                )
                [ TermVar
                    ( NamedVar "x" )
                , TermVar
                    ( NamedVar "y" )
                ]
            )
        )
    )
, BlockProof
    ( SourcePos
        { sourceName = "test/examples/proofdefinefunction.tex"
        , sourceLine = Pos 25
        , sourceColumn = Pos 1
        }
    )
    ( DefineFunction
        ( NamedVar "f" )
        ( NamedVar "z" )
        ( TermVar
            ( NamedVar "z" )
        )
        ( TermVar
            ( NamedVar "x" )
        ) ( Qed JustificationEmpty )
    )
]