[ BlockInductive
    ( Location
        { locFile = "test/examples/inductive.tex"
        , locLine = 3
        , locColumn = 1
        }
    ) Nothing
    ( Marker "fin" )
    ( Inductive
        { inductiveSymbolPattern = SymbolPattern
            ( MixfixItem
                ( TokenCons
                    ( Command "fin" )
                    ( TokenCons InvisibleBraceL
                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
                    )
                )
                ( Marker "fin" ) NonAssoc
            )
            [ NamedVar "A" ]
        , inductiveDomain = ExprOp
            ( Location
                { locFile = "test/examples/inductive.tex"
                , locLine = 4
                , locColumn = 29
                }
            )
            ( MixfixItem
                ( TokenCons
                    ( Command "cumul" )
                    ( TokenCons InvisibleBraceL
                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
                    )
                )
                ( Marker "cumul" ) NonAssoc
            )
            [ ExprVar
                ( NamedVar "A" )
            ]
        , inductiveIntros = IntroRule
            { introConditions = []
            , introResult = FormulaChain
                ( ChainBase
                    ( ExprVar
                        ( NamedVar "A" ) :| []
                    ) Positive
                    ( Relation
                        ( Location
                            { locFile = "test/examples/inductive.tex"
                            , locLine = 6
                            , locColumn = 17
                            }
                        )
                        ( RelationSymbol
                            ( Command "in" )
                            ( ParameterArity 0 )
                            ( Marker "elem" )
                        ) []
                    )
                    ( ExprOp
                        ( Location
                            { locFile = "test/examples/inductive.tex"
                            , locLine = 6
                            , locColumn = 20
                            }
                        )
                        ( MixfixItem
                            ( TokenCons
                                ( Command "fin" )
                                ( TokenCons InvisibleBraceL
                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
                                )
                            )
                            ( Marker "fin" ) NonAssoc
                        )
                        [ ExprVar
                            ( NamedVar "A" )
                        ] :| []
                    )
                )
            } :| []
        }
    )
]