Check direct inductives through fixed-point replay

11 files changed, 679 insertions, 4736 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index 3a50fd7..e94aa3f 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -23,6 +23,7 @@ import Checking.Obligation
 import Checking.Structure qualified as Structure
 import Checking.Transition qualified as Transition
 import Checking.Typed.Atomic qualified as TypedAtomic
+import Checking.Typed.Inductive qualified as TypedInductive
 import Checking.Typed.Reflexivity qualified as TypedReflexivity
 import StructGraph
 import Syntax.Internal
@@ -444,6 +445,7 @@ builtinReservedMixfixMarkers :: Set Marker
 builtinReservedMixfixMarkers =
     Set.fromList
         [ "cons"
+        , "cumul"
         , "emptyset"
         , "naturals"
         , "pair"
@@ -3139,6 +3141,22 @@ checkInductive context inductive = do
             (SymbolMixfix (inductiveSymbol inductive))
             st)
     checked <- normalizeInductive inductive
+    case checkingTransitionModuleBuilder st of
+        Nothing ->
+            checkLegacyInductive context checked st
+        Just builder ->
+            checkTypedInductive
+                context
+                checked
+                builder
+                st
+
+checkLegacyInductive
+    :: BlockContext
+    -> CheckedInductive
+    -> CheckingState
+    -> Checking
+checkLegacyInductive context checked st = do
     soundnessGoals <-
         traverse canonicalize (inductiveSoundnessGoals checked)
     stagedFacts <-
@@ -3175,6 +3193,283 @@ checkInductive context inductive = do
             <$> inductiveFactRoles checked
         )
 
+checkTypedInductive
+    :: BlockContext
+    -> CheckedInductive
+    -> Transition.TransitionModuleBuilder
+    -> CheckingState
+    -> Checking
+checkTypedInductive context checked builder st = do
+    direct <-
+        either
+            throwIO
+            pure
+            (directInductive context checked)
+    prepared <-
+        either
+            ( throwIO
+                . typedInductiveError
+                    context
+                    "typed inductive preparation failed: "
+            )
+            pure
+            (TypedInductive.prepareTypedInductive
+                (Transition.transitionBuilderFoundation
+                    builder)
+                (typedSourceGlobal builder)
+                (blockContextMarker context)
+                direct)
+    imports <-
+        Vector.fromList
+            <$> traverse
+                (uncurry
+                    (typedInductiveGuardImport
+                        context
+                        builder))
+                (zip
+                    [1 :: Int ..]
+                    (Vector.toList
+                        (TypedInductive.typedInductiveGuardTargets
+                            prepared)))
+    builderWithCarrier <-
+        either
+            ( throwIO
+                . typedInductiveError
+                    context
+                    "typed inductive carrier registration failed: "
+            )
+            pure
+            (Transition.commitTransitionTransparentGlobal
+                (SymbolMixfix
+                    (checkedInductiveSymbol checked))
+                (TypedInductive.typedInductiveCarrierType
+                    prepared)
+                (TypedInductive.typedInductiveCarrierBody
+                    prepared)
+                (typedFactOrigin context)
+                builder)
+    builder' <-
+        foldM
+            (commitTypedInductiveFact
+                context
+                imports)
+            builderWithCarrier
+            (TypedInductive.typedInductiveFacts
+                prepared)
+    committed <-
+        either
+            throwIO
+            pure
+            (commitTypedInductiveState
+                context
+                checked
+                (TypedInductive.typedInductiveFactMarker
+                    <$> TypedInductive.typedInductiveFacts
+                        prepared)
+                builder'
+                st)
+    putDeclarationCandidate committed
+    setDeclarationFactProducers []
+
+directInductive
+    :: BlockContext
+    -> CheckedInductive
+    -> Either CheckingError TypedInductive.DirectInductive
+directInductive context checked =
+    TypedInductive.DirectInductive
+        (checkedInductiveParams checked)
+        (checkedInductiveDomain checked)
+        <$> traverse directClause
+            (checkedInductiveIntros checked)
+  where
+    directClause intro =
+        TypedInductive.DirectInductiveClause
+            (checkedInductiveIntroVars intro)
+            <$> traverse directCondition
+                (checkedInductiveIntroConditions intro)
+            <*> pure
+                (checkedInductiveIntroResultTerm intro)
+
+    directCondition = \case
+        CheckedInductiveSideCondition formula ->
+            Right
+                (TypedInductive.DirectSideCondition
+                    formula)
+        CheckedInductiveRecursiveCondition
+                { checkedInductiveRecursiveTerm
+                , checkedInductiveRecursiveDirect = True
+                } ->
+            Right
+                (TypedInductive.DirectRecursiveCondition
+                    checkedInductiveRecursiveTerm)
+        CheckedInductiveRecursiveCondition{} ->
+            Left
+                (checkingErrorAt context
+                    "nested inductive recursion is not supported by the typed set-valued inductive slice")
+
+typedSourceGlobal
+    :: Transition.TransitionModuleBuilder
+    -> Symbol
+    -> Maybe TypedInductive.SourceGlobal
+typedSourceGlobal builder symbol = do
+    reference <-
+        Transition.lookupTransitionGlobal
+            symbol
+            builder
+    pure
+        (TypedInductive.SourceGlobal
+            reference
+            (Transition.lookupTransitionGlobalBody
+                symbol
+                builder))
+
+typedInductiveGuardImport
+    :: BlockContext
+    -> Transition.TransitionModuleBuilder
+    -> Int
+    -> Core.FrozenCheckedCore
+        Transition.CheckedGlobalRef
+    -> CheckingM Transition.TransitionDerivationImport
+typedInductiveGuardImport
+        context
+        builder
+        ordinal
+        target = do
+    found <-
+        either
+            ( throwIO
+                . typedInductiveError
+                    context
+                    "typed inductive guard lookup failed: "
+            )
+            pure
+            (Transition.lookupTransitionTypedImport
+                target
+                builder)
+    maybe
+        (throwIO
+            (checkingErrorAt context
+                ( "typed inductive domain guard "
+                    <> Text.pack (show ordinal)
+                    <> " has no authorized typed fact"
+                )))
+        pure
+        found
+
+commitTypedInductiveFact
+    :: BlockContext
+    -> Vector Transition.TransitionDerivationImport
+    -> Transition.TransitionModuleBuilder
+    -> TypedInductive.PreparedTypedInductiveFact
+    -> CheckingM Transition.TransitionModuleBuilder
+commitTypedInductiveFact context imports builder fact = do
+    admitted <-
+        either
+            ( throwIO
+                . typedInductiveError
+                    context
+                    "typed inductive replay failed: "
+            )
+            pure
+            (Transition.authorizeTransitionKernelFactWithImports
+                imports
+                (TypedInductive.typedInductiveFactTarget
+                    fact)
+                (TypedInductive.typedInductiveFactDerivation
+                    fact)
+                builder)
+    either
+        ( throwIO
+            . typedInductiveError
+                context
+                "typed inductive fact registration failed: "
+        )
+        pure
+        (Transition.commitTransitionTypedFact
+            (TypedInductive.typedInductiveFactMarker
+                fact
+                :| [])
+            (typedFactOrigin context)
+            admitted
+            builder)
+
+commitTypedInductiveState
+    :: BlockContext
+    -> CheckedInductive
+    -> NonEmpty Marker
+    -> Transition.TransitionModuleBuilder
+    -> CheckingState
+    -> Either CheckingError CheckingState
+commitTypedInductiveState
+        context
+        checked
+        factMarkers
+        builder
+        st = do
+    markers' <-
+        validatedMarkers
+            location
+            (marker : NonEmpty.toList factMarkers)
+            st
+    (owners', ownedMarkers', dependencies') <-
+        validatedSymbolRegistration
+            context
+            OwnedByInductiveDefinition
+            carrier
+            mempty
+            st
+    frozenSymbols <-
+        first
+            ( checkingErrorAt context
+                . ("inductive specification mentions unknown symbol " <>)
+                . symbolText
+            )
+            (checkedInductiveFrozenSymbols
+                dependencies'
+                checked)
+    let frozen =
+            HM.fromList
+                [ (symbol, marker)
+                | symbol <- Set.toList frozenSymbols
+                , ownableSymbol symbol
+                ]
+    pure
+        st
+            { checkingDependencies = dependencies'
+            , checkingOwnedSymbols = owners'
+            , checkingOwnedSymbolMarkers = ownedMarkers'
+            , checkingFrozenSymbols =
+                HM.union
+                    (checkingFrozenSymbols st)
+                    frozen
+            , definedMarkers = markers'
+            , blockLabel = marker
+            , stepLocation = location
+            , checkingHypothesisCounter = 0
+            , checkingTransitionModuleBuilder =
+                Just builder
+            }
+  where
+    location =
+        blockContextLocation context
+    marker =
+        blockContextMarker context
+    carrier =
+        SymbolMixfix
+            (checkedInductiveSymbol checked)
+
+typedInductiveError
+    :: Show error
+    => BlockContext
+    -> Text
+    -> error
+    -> CheckingError
+typedInductiveError context prefix =
+    checkingErrorAt context
+        . (prefix <>)
+        . Text.pack
+        . show
+
 validateInductiveHeader
     :: BlockContext
     -> Symbol
diff --git a/source/Checking/Transition.hs b/source/Checking/Transition.hs
index 4fe7d5d..8802f90 100644
--- a/source/Checking/Transition.hs
+++ b/source/Checking/Transition.hs
@@ -59,13 +59,16 @@ module Checking.Transition
     , openTransitionModuleBuilder
     , transitionBuilderLegacyStage
     , transitionBuilderImportedCheckingEnvironment
+    , transitionBuilderFoundation
     , beginTransitionDeclaration
     , transitionCurrentDeclarationReference
     , commitTransitionOpaqueGlobal
+    , commitTransitionTransparentGlobal
     , commitTransitionTypedFact
     , commitTransitionTypedDeclaredAssumption
     , transitionBuilderWithLegacyStage
     , lookupTransitionGlobal
+    , lookupTransitionGlobalBody
     , TransitionAdmittedModule
     , sealTransitionModule
     , transitionAdmittedName
@@ -74,7 +77,7 @@ module Checking.Transition
     , transitionAdmittedKernelProofCount
     , transitionAdmittedTypedDirectAxiomManifest
     , transitionAdmittedTypedTrustDependencies
-    , transitionAdmittedOpaqueGlobals
+    , transitionAdmittedGlobals
     , TransitionModuleError(..)
     ) where
 
@@ -707,7 +710,25 @@ data TypedGlobalBinding = TypedGlobalBinding
     !Symbol
     !CheckedGlobalRef
     !Origin
-    deriving stock (Show, Eq)
+    !(Maybe (FrozenCheckedCore CheckedGlobalRef))
+    deriving stock (Eq)
+
+instance Show TypedGlobalBinding where
+    show
+            (TypedGlobalBinding
+                symbol
+                reference
+                bindingOrigin
+                body) =
+        "TypedGlobalBinding "
+            <> show symbol
+            <> " "
+            <> show reference
+            <> " "
+            <> show bindingOrigin
+            <> if isJust body
+                then " Transparent"
+                else " Opaque"
 
 data TypedModuleEnvironmentDelta =
     TypedModuleEnvironmentDelta
@@ -797,6 +818,12 @@ transitionBuilderImportedCheckingEnvironment =
     legacyStageImportedCheckingEnvironment
         . transitionBuilderLegacyStage
 
+transitionBuilderFoundation
+    :: TransitionModuleBuilder
+    -> CheckedFoundation
+transitionBuilderFoundation =
+    builderFoundation
+
 beginTransitionDeclaration
     :: TransitionModuleBuilder
     -> TransitionModuleBuilder
@@ -834,6 +861,72 @@ commitTransitionOpaqueGlobal
         coreType
         bindingOrigin
         builder =
+    commitTransitionGlobal
+        symbol
+        coreType
+        bindingOrigin
+        Nothing
+        builder
+
+commitTransitionTransparentGlobal
+    :: Symbol
+    -> CoreType
+    -> FrozenCheckedCore CheckedGlobalRef
+    -> Origin
+    -> TransitionModuleBuilder
+    -> Either TransitionModuleError TransitionModuleBuilder
+commitTransitionTransparentGlobal
+        symbol
+        coreType
+        body
+        bindingOrigin
+        builder = do
+    unless
+        (frozenCoreType body == coreType)
+        (Left
+            (TransitionTransparentGlobalTypeMismatch
+                symbol
+                coreType
+                (frozenCoreType body)))
+    let visibleReferences =
+            Set.fromList
+                [ reference
+                | TypedGlobalBinding
+                    _visibleSymbol
+                    reference
+                    _visibleOrigin
+                    _visibleBody <-
+                        Map.elems (builderGlobals builder)
+                ]
+        unavailable =
+            frozenCoreGlobals body
+                `Set.difference` visibleReferences
+    unless
+        (Set.null unavailable)
+        (Left
+            (TransitionTransparentGlobalDependencyNotVisible
+                symbol
+                unavailable))
+    commitTransitionGlobal
+        symbol
+        coreType
+        bindingOrigin
+        (Just body)
+        builder
+
+commitTransitionGlobal
+    :: Symbol
+    -> CoreType
+    -> Origin
+    -> Maybe (FrozenCheckedCore CheckedGlobalRef)
+    -> TransitionModuleBuilder
+    -> Either TransitionModuleError TransitionModuleBuilder
+commitTransitionGlobal
+        symbol
+        coreType
+        bindingOrigin
+        body
+        builder =
     case transitionCurrentDeclarationReference builder of
         Nothing ->
             Left TransitionDeclarationNotOpen
@@ -843,9 +936,10 @@ commitTransitionOpaqueGlobal
                 Just (TypedGlobalBinding
                     _previousSymbol
                     previousReference
-                    previousOrigin) ->
+                    previousOrigin
+                    _previousBody) ->
                         Left
-                            (TransitionOpaqueGlobalConflict
+                            (TransitionGlobalConflict
                                 symbol
                                 previousReference
                                 previousOrigin
@@ -874,6 +968,7 @@ commitTransitionOpaqueGlobal
                         reference
                         coreType)
                     bindingOrigin
+                    body
 
 commitTransitionTypedFact
     :: NonEmpty Marker
@@ -1079,8 +1174,25 @@ lookupTransitionGlobal symbol builder =
         <$> Map.lookup symbol (builderGlobals builder)
   where
     bindingReference
-        (TypedGlobalBinding _symbol reference _origin) =
+        (TypedGlobalBinding
+            _symbol
             reference
+            _origin
+            _body) =
+            reference
+
+lookupTransitionGlobalBody
+    :: Symbol
+    -> TransitionModuleBuilder
+    -> Maybe (FrozenCheckedCore CheckedGlobalRef)
+lookupTransitionGlobalBody symbol builder = do
+    TypedGlobalBinding
+        _bindingSymbol
+        _reference
+        _origin
+        body <-
+            Map.lookup symbol (builderGlobals builder)
+    body
 
 
 data TransitionAdmittedModule = TransitionAdmittedModule
@@ -1206,12 +1318,16 @@ transitionAdmittedTypedTrustDependencies =
             . admittedFactTypedTrustDependencies)
         . transitionAdmittedFacts
 
-transitionAdmittedOpaqueGlobals
+transitionAdmittedGlobals
     :: TransitionAdmittedModule
     -> Vector (Symbol, CheckedGlobalRef, Origin)
-transitionAdmittedOpaqueGlobals admitted =
+transitionAdmittedGlobals admitted =
     fmap
-        (\(TypedGlobalBinding symbol reference bindingOrigin) ->
+        (\(TypedGlobalBinding
+                symbol
+                reference
+                bindingOrigin
+                _body) ->
             (symbol, reference, bindingOrigin))
         (admittedLocalGlobals admitted)
 
@@ -1321,7 +1437,8 @@ mergeTypedEnvironments directImports = do
             binding@(TypedGlobalBinding
                 symbol
                 reference
-                bindingOrigin) =
+                bindingOrigin
+                _body) =
         case Map.lookup symbol globals of
             Nothing ->
                 Right (Map.insert symbol binding globals)
@@ -1329,12 +1446,13 @@ mergeTypedEnvironments directImports = do
                 (TypedGlobalBinding
                     _previousSymbol
                     previousReference
-                    previousOrigin)
+                    previousOrigin
+                    _previousBody)
                 | previousReference == reference ->
                     Right globals
                 | otherwise ->
                     Left
-                        (TransitionOpaqueGlobalConflict
+                        (TransitionGlobalConflict
                             symbol
                             previousReference
                             previousOrigin
@@ -1450,12 +1568,19 @@ data TransitionModuleError
     | TransitionDeclarationNotOpen
     | TransitionImportedModuleConflict
         !ModuleName
-    | TransitionOpaqueGlobalConflict
+    | TransitionGlobalConflict
         !Symbol
         !CheckedGlobalRef
         !Origin
         !CheckedGlobalRef
         !Origin
+    | TransitionTransparentGlobalTypeMismatch
+        !Symbol
+        !CoreType
+        !CoreType
+    | TransitionTransparentGlobalDependencyNotVisible
+        !Symbol
+        !(Set CheckedGlobalRef)
     | TransitionTypedFactIsNotProposition
         !CoreType
     | TransitionKernelTargetMismatch
diff --git a/source/Test/Unit/Source.hs b/source/Test/Unit/Source.hs
index 0a5319e..dc9c901 100644
--- a/source/Test/Unit/Source.hs
+++ b/source/Test/Unit/Source.hs
@@ -37,7 +37,7 @@ import Syntax.Internal
 import Syntax.Token (runLexer)
 
 import Bound.Scope (toScope)
-import Control.Exception (bracket, evaluate)
+import Control.Exception (bracket, evaluate, try)
 import Data.ByteString qualified as ByteString
 import Data.HashMap.Strict qualified as HashMap
 import Data.IORef
@@ -94,6 +94,8 @@ unitTests = testGroup "Source resolution"
         publishesLegacyImportViews
     , testCase "publishes typed signatures and facts through transition modules"
         publishesTransitionSignatures
+    , testCase "enforces and replays direct inductive guards"
+        publishesTypedInductive
     , testCase "shares one closure syntax world across modules"
         sharesClosureSyntaxWorld
     , testCase "canonicalizes syntax deltas independently of traversal"
@@ -809,7 +811,7 @@ publishesTransitionSignatures =
                             (Axiom [] sharedAtomicFormula)
                         ]
                 let sharedGlobals =
-                        Transition.transitionAdmittedOpaqueGlobals
+                        Transition.transitionAdmittedGlobals
                             shared
                 assertEqual
                     "one shared typed declaration"
@@ -951,7 +953,7 @@ publishesTransitionSignatures =
                                     (EmptySet Nowhere)))
                         ]
                 case Vector.toList
-                        (Transition.transitionAdmittedOpaqueGlobals
+                        (Transition.transitionAdmittedGlobals
                             entry) of
                     [(_symbol, reference, _origin)] ->
                         assertEqual
@@ -1085,6 +1087,210 @@ publishesTransitionSignatures =
                 (Checking.checkingStateEnvironment checked)
                 finalBuilder)
 
+publishesTypedInductive :: Assertion
+publishesTypedInductive =
+    withTemporaryDirectory "felix-transition-inductive" \temp -> do
+        writeTheory
+            (temp Posix.</> "entry.tex")
+            []
+            "entry"
+        graph <- buildSearchedGraph temp "entry.tex"
+        workspace <-
+            expectRight
+                =<< Parse.parseResolvedSourceGraph graph
+        assignments <-
+            expectRight
+                (Legacy.assignLegacyModuleOrdinals
+                    workspace)
+        assignment <-
+            case toList assignments of
+                [only] ->
+                    pure only
+                actual ->
+                    assertFailure
+                        ("expected one module assignment, got "
+                            <> show (length actual))
+                        >> fail "unreachable"
+        checkedFoundationValue <-
+            expectRight Foundation.checkedFoundation
+        builder <-
+            expectRight
+                (Transition.openTransitionModuleBuilder
+                    checkedFoundationValue
+                    Checking.initialLegacyCheckingEnvironment
+                    assignment
+                    [])
+        let unprovedCarrier =
+                TermOp Nowhere unprovedInductiveSymbol []
+            unprovedBlocks =
+                [ BlockInductive
+                    Nowhere
+                    "unproved_inductive"
+                    Inductive
+                        { inductiveSymbol =
+                            unprovedInductiveSymbol
+                        , inductiveParams = []
+                        , inductiveDomain =
+                            EmptySet Nowhere
+                        , inductiveIntros =
+                            IntroRule
+                                []
+                                ( EmptySet Nowhere
+                                    `isElementOf`
+                                        unprovedCarrier
+                                )
+                                :| []
+                        }
+                ]
+        unproved <-
+            try
+                (Checking.runCheckingBlocks
+                    unprovedBlocks
+                    (Checking.initialTransitionCheckingStateWithTaskPreparation
+                        Checking.WithoutDumpPremselTraining
+                        id
+                        builder
+                        (\_batch ->
+                            assertFailure
+                                "unproved inductive emitted a legacy obligation")))
+                :: IO
+                    (Either
+                        Checking.CheckingError
+                        Checking.CheckingState)
+        case unproved of
+            Left checkingError ->
+                assertBool
+                    "missing exact guard is reported"
+                    ("has no authorized typed fact"
+                        `Text.isInfixOf`
+                            Text.pack (show checkingError))
+            Right _checked ->
+                assertFailure
+                    "inductive with an unproved domain guard was admitted"
+        unchanged <-
+            expectRight
+                (Transition.sealTransitionModule
+                    Checking.initialLegacyCheckingEnvironment
+                    builder)
+        assertEqual
+            "failed inductive publishes no global"
+            0
+            (Vector.length
+                (Transition.transitionAdmittedGlobals
+                    unchanged))
+        assertEqual
+            "failed inductive publishes no fact"
+            0
+            (Vector.length
+                (Transition.transitionAdmittedFacts
+                    unchanged))
+        let parameter =
+                NamedVar "domain"
+            domain =
+                TermOp
+                    Nowhere
+                    cumulSymbol
+                    [TermVar parameter]
+            carrier =
+                TermOp
+                    Nowhere
+                    typedInductiveSymbol
+                    [TermVar parameter]
+            blocks =
+                [ BlockInductive
+                    Nowhere
+                    "typed_inductive"
+                    Inductive
+                        { inductiveSymbol =
+                            typedInductiveSymbol
+                        , inductiveParams = [parameter]
+                        , inductiveDomain = domain
+                        , inductiveIntros =
+                            IntroRule
+                                []
+                                (TermVar parameter
+                                    `isElementOf`
+                                        carrier)
+                                :| []
+                        }
+                ]
+        checked <-
+            Checking.runCheckingBlocks
+                blocks
+                (Checking.initialTransitionCheckingStateWithTaskPreparation
+                    Checking.WithoutDumpPremselTraining
+                    id
+                    builder
+                    (\_batch ->
+                        assertFailure
+                            "typed inductive emitted a legacy obligation"))
+        finalBuilder <-
+            maybe
+                (assertFailure
+                    "checking lost its transition builder"
+                    >> fail "unreachable")
+                pure
+                (Checking.checkingTransitionModuleBuilder
+                    checked)
+        admitted <-
+            expectRight
+                (Transition.sealTransitionModule
+                    (Checking.checkingStateEnvironment
+                        checked)
+                    finalBuilder)
+        assertEqual
+            "one transparent carrier"
+            1
+            (Vector.length
+                (Transition.transitionAdmittedGlobals
+                    admitted))
+        assertEqual
+            "four derived facts"
+            [True, True, True, True]
+            ( Transition.admittedFactIsKernelProof
+                <$> Vector.toList
+                    (Transition.transitionAdmittedFacts
+                        admitted)
+            )
+        assertEqual
+            "four replayed inductive facts"
+            4
+            (Transition.transitionAdmittedKernelProofCount
+                admitted)
+        assertBool
+            "foundation guard dependency is retained"
+            (Foundation.UnivOfContains
+                `Set.member`
+                    Transition.typedFoundationUses
+                        (Transition.transitionAdmittedTypedTrustDependencies
+                            admitted))
+  where
+    typedInductiveSymbol =
+        mkMixfixItem
+            [ Just (Command "typedfin")
+            , Just InvisibleBraceL
+            , Nothing
+            , Just InvisibleBraceR
+            ]
+            "typed_inductive"
+            NonAssoc
+
+    cumulSymbol =
+        mkMixfixItem
+            [ Just (Command "cumul")
+            , Just InvisibleBraceL
+            , Nothing
+            , Just InvisibleBraceR
+            ]
+            "cumul"
+            NonAssoc
+
+    unprovedInductiveSymbol =
+        mkMixfixItem
+            [Just (Command "unprovedfin")]
+            "unproved_inductive"
+            NonAssoc
+
 publishesLegacyImportViews :: Assertion
 publishesLegacyImportViews =
     withTemporaryDirectory "felix-legacy-import-view" \temp -> do
diff --git a/test/examples/inductive.tex b/test/examples/inductive.tex
index 20c1aa7..0ec5a51 100644
--- a/test/examples/inductive.tex
+++ b/test/examples/inductive.tex
@@ -1,43 +1,8 @@
-% Compact inductive examples covering derived facts and soundness tasks
-
-% Generated inductive subset facts are expanded elementwise by the checker.
-%
-%
-
-\begin{axiom}\label{pow}
-    $\pow{A} = \emptyset$.
-\end{axiom}
-
-\begin{axiom}\label{cons}
-    $\cons{a}{B} = \emptyset$.
-\end{axiom}
-
-\begin{definition}\label{wrap}
-    $\wrap{A} = \emptyset$.
-\end{definition}
-
-\begin{axiom}\label{everything_in_emptyset}
-    $x\in\emptyset$.
-\end{axiom}
+% Direct bounded inductive example checked through the typed fixed-point path.
 
 \begin{inductive}\label{fin}
-    Define $\fin{A}\subseteq\pow{A}$ inductively as follows.
-    \begin{enumerate}
-        \item $\emptyset \in\fin{A}$.
-        \item If $a\in A$ and $B\in\fin{A}$, then $\cons{a}{B}\in\fin{A}$.
-    \end{enumerate}
-\end{inductive}
-
-\begin{proposition}\label{fin_intro_ref}
-    $\emptyset \in \fin{A}$.
-\end{proposition}
-\begin{proof}
-    Follows by \ref{fin_intro_1}.
-\end{proof}
-
-\begin{inductive}\label{acc}
-    Define $\acc{R}\subseteq\wrap{R}$ inductively as follows.
+    Define $\fin{A}\subseteq\cumul{A}$ inductively as follows.
     \begin{enumerate}
-        \item If $x\in\wrap{\acc{R}}$, then $x\in\acc{R}$.
+        \item $A\in\fin{A}$.
     \end{enumerate}
 \end{inductive}
diff --git a/test/golden/inductive/encoding tasks.golden b/test/golden/inductive/encoding tasks.golden
index fae5b95..af2aad1 100644
--- a/test/golden/inductive/encoding tasks.golden
+++ b/test/golden/inductive/encoding tasks.golden
@@ -1,38 +1 @@
-fof(zf_q0,conjecture,![V0]:zf_u4(zf_u1,zf_u2(V0))).
-fof(zf_h0,axiom,![V1,V2]:zf_u0(V1,V2)=zf_u1).
-fof(zf_h1,axiom,![V3]:zf_u2(V3)=zf_u1).
-fof(zf_h2,axiom,![V4]:zf_u3(V4)=zf_u1).
-fof(zf_h3,axiom,![V5]:zf_u4(V5,zf_u1)).
-------------------
-fof(zf_q0,conjecture,![V0,V1,V2]:((zf_u4(V0,V1)&zf_u4(V2,zf_u2(V1)))=>zf_u4(zf_u0(V0,V2),zf_u2(V1)))).
-fof(zf_h0,axiom,![V3,V4]:zf_u0(V3,V4)=zf_u1).
-fof(zf_h1,axiom,![V5]:zf_u2(V5)=zf_u1).
-fof(zf_h2,axiom,![V6]:zf_u3(V6)=zf_u1).
-fof(zf_h3,axiom,![V7]:zf_u4(V7,zf_u1)).
-------------------
-fof(zf_q0,conjecture,zf_u2(zf_u0,zf_u1(zf_f0))).
-fof(zf_h0,axiom,![V0]:zf_u2(zf_u0,zf_u1(V0))).
-------------------
-fof(zf_q0,conjecture,![V0,V1]:(![V2]:(zf_u5(V2,V0)=>zf_u5(V2,V1))=>![V3]:(zf_u5(V3,zf_u4(V0))=>zf_u5(V3,zf_u4(V1))))).
-fof(zf_h0,axiom,![V4,V5,V6]:((zf_u5(V4,V5)&zf_u5(V6,zf_u2(V5)))=>zf_u5(zf_u0(V4,V6),zf_u2(V5)))).
-fof(zf_h1,axiom,![V7,V8]:((zf_u5(zf_u1,V7)&![V9,V10]:((zf_u5(V9,V8)&zf_u5(V10,V7))=>zf_u5(zf_u0(V9,V10),V7)))=>![V11]:(zf_u5(V11,zf_u2(V8))=>zf_u5(V11,V7)))).
-fof(zf_h2,axiom,![V12,V13]:(zf_u5(V12,zf_u2(V13))=>(V12=zf_u1|?[V14,V15]:(zf_u5(V14,V13)&zf_u5(V15,zf_u2(V13))&V12=zf_u0(V14,V15))))).
-fof(zf_h3,axiom,![V16,V17]:zf_u0(V16,V17)=zf_u1).
-fof(zf_h4,axiom,![V18]:![V19]:(zf_u5(V19,zf_u2(V18))=>zf_u5(V19,zf_u3(V18)))).
-fof(zf_h5,axiom,![V20]:zf_u3(V20)=zf_u1).
-fof(zf_h6,axiom,![V21]:zf_u4(V21)=zf_u1).
-fof(zf_h7,axiom,![V22]:zf_u5(V22,zf_u1)).
-fof(zf_h8,axiom,![V23]:zf_u5(zf_u1,zf_u2(V23))).
-fof(zf_h9,axiom,![V24]:zf_u5(zf_u1,zf_u2(V24))).
-------------------
-fof(zf_q0,conjecture,![V0,V1]:(zf_u5(V0,zf_u4(zf_u4(V1)))=>zf_u5(V0,zf_u4(V1)))).
-fof(zf_h0,axiom,![V2,V3,V4]:((zf_u5(V2,V3)&zf_u5(V4,zf_u2(V3)))=>zf_u5(zf_u0(V2,V4),zf_u2(V3)))).
-fof(zf_h1,axiom,![V5,V6]:((zf_u5(zf_u1,V5)&![V7,V8]:((zf_u5(V7,V6)&zf_u5(V8,V5))=>zf_u5(zf_u0(V7,V8),V5)))=>![V9]:(zf_u5(V9,zf_u2(V6))=>zf_u5(V9,V5)))).
-fof(zf_h2,axiom,![V10,V11]:(zf_u5(V10,zf_u2(V11))=>(V10=zf_u1|?[V12,V13]:(zf_u5(V12,V11)&zf_u5(V13,zf_u2(V11))&V10=zf_u0(V12,V13))))).
-fof(zf_h3,axiom,![V14,V15]:zf_u0(V14,V15)=zf_u1).
-fof(zf_h4,axiom,![V16]:![V17]:(zf_u5(V17,zf_u2(V16))=>zf_u5(V17,zf_u3(V16)))).
-fof(zf_h5,axiom,![V18]:zf_u3(V18)=zf_u1).
-fof(zf_h6,axiom,![V19]:zf_u4(V19)=zf_u1).
-fof(zf_h7,axiom,![V20]:zf_u5(V20,zf_u1)).
-fof(zf_h8,axiom,![V21]:zf_u5(zf_u1,zf_u2(V21))).
-fof(zf_h9,axiom,![V22]:zf_u5(zf_u1,zf_u2(V22))).
\ No newline at end of file
+fof(zf_q0,conjecture,![V0]:zf_u1(V0,zf_u0(V0))).
\ No newline at end of file
diff --git a/test/golden/inductive/generating tasks.golden b/test/golden/inductive/generating tasks.golden
index fb51bdc..18cb929 100644
--- a/test/golden/inductive/generating tasks.golden
+++ b/test/golden/inductive/generating tasks.golden
@@ -1,238 +1,10 @@
 [ Task
     { taskDirectness = Direct
-    , taskHypotheses =
-        [ Hypothesis Marker "everything_in_emptyset" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 20
-                        , locColumn = 7
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermVar
-                        ( B
-                            ( NamedVar "x" )
-                        )
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 20
-                            , locColumn = 10
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "wrap" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 16
-                            , locColumn = 17
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "cons" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 12
-                        , locColumn = 18
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "cons" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons
-                                            ( TokenCons InvisibleBraceR
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                        )
-                                    )
-                                )
-                                ( Marker "cons" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "a" )
-                            )
-                        , TermVar
-                            ( B
-                                ( NamedVar "B" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "pow" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 8
-                        , locColumn = 14
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "pow" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "pow" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 16
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        ]
+    , taskHypotheses = []
     , taskConjectureLabel = Marker "fin"
     , taskLocation = Location
         { locFile = "test/examples/inductive.tex"
-        , locLine = 23
+        , locLine = 3
         , locColumn = 1
         }
     , taskConjecture = Quantified Universally
@@ -253,37 +25,26 @@
                         )
                     )
                 )
-                [ TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 26
-                        , locColumn = 16
-                        }
+                [ TermVar
+                    ( B
+                        ( NamedVar "A" )
                     )
-                    ( SymbolMixfix
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "emptyset" ) End
-                            )
-                            ( Marker "emptyset" ) NonAssoc
-                        )
-                    ) []
                 , TermSymbol
                     ( Location
                         { locFile = "test/examples/inductive.tex"
-                        , locLine = 24
+                        , locLine = 4
                         , locColumn = 29
                         }
                     )
                     ( SymbolMixfix
                         ( MixfixItem
                             ( TokenCons
-                                ( Command "pow" )
+                                ( Command "cumul" )
                                 ( TokenCons InvisibleBraceL
                                     ( HoleCons ( TokenCons InvisibleBraceR End ) )
                                 )
                             )
-                            ( Marker "pow" ) NonAssoc
+                            ( Marker "cumul" ) NonAssoc
                         )
                     )
                     [ TermVar
@@ -295,3018 +56,4 @@
             )
         )
     }
-, Task
-    { taskDirectness = Direct
-    , taskHypotheses =
-        [ Hypothesis Marker "everything_in_emptyset" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 20
-                        , locColumn = 7
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermVar
-                        ( B
-                            ( NamedVar "x" )
-                        )
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 20
-                            , locColumn = 10
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "wrap" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 16
-                            , locColumn = 17
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "cons" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 12
-                        , locColumn = 18
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "cons" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons
-                                            ( TokenCons InvisibleBraceR
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                        )
-                                    )
-                                )
-                                ( Marker "cons" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "a" )
-                            )
-                        , TermVar
-                            ( B
-                                ( NamedVar "B" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "pow" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 8
-                        , locColumn = 14
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "pow" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "pow" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 16
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        ]
-    , taskConjectureLabel = Marker "fin"
-    , taskLocation = Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 23
-        , locColumn = 1
-        }
-    , taskConjecture = Quantified Universally
-        ( Scope
-            ( Connected Implication
-                ( Connected Conjunction
-                    ( TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 27
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "a" )
-                            )
-                        , TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    )
-                    ( TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "B" )
-                            )
-                        , TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 24
-                                , locColumn = 29
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "pow" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "pow" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "A" )
-                                )
-                            ]
-                        ]
-                    )
-                )
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 27
-                            , locColumn = 52
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "cons" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons
-                                            ( TokenCons InvisibleBraceR
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                        )
-                                    )
-                                )
-                                ( Marker "cons" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "a" )
-                            )
-                        , TermVar
-                            ( B
-                                ( NamedVar "B" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 24
-                            , locColumn = 29
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "pow" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "pow" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    ]
-                )
-            )
-        )
-    }
-, Task
-    { taskDirectness = Direct
-    , taskHypotheses =
-        [ Hypothesis Marker "fin_intro_1" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 26
-                            , locColumn = 16
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    , TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "fin" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "fin" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    ]
-                )
-            )
-        ]
-    , taskConjectureLabel = Marker "fin_intro_ref"
-    , taskLocation = Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 35
-        , locColumn = 5
-        }
-    , taskConjecture = TermSymbol
-        ( Location
-            { locFile = "test/examples/inductive.tex"
-            , locLine = 32
-            , locColumn = 16
-            }
-        )
-        ( SymbolPredicate
-            ( PredicateRelation
-                ( RelationSymbol
-                    ( Command "in" )
-                    ( ParameterArity 0 )
-                    ( Marker "elem" )
-                )
-            )
-        )
-        [ TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 32
-                , locColumn = 6
-                }
-            )
-            ( SymbolMixfix
-                ( MixfixItem
-                    ( TokenCons
-                        ( Command "emptyset" ) End
-                    )
-                    ( Marker "emptyset" ) NonAssoc
-                )
-            ) []
-        , TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 32
-                , locColumn = 20
-                }
-            )
-            ( SymbolMixfix
-                ( MixfixItem
-                    ( TokenCons
-                        ( Command "fin" )
-                        ( TokenCons InvisibleBraceL
-                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                        )
-                    )
-                    ( Marker "fin" ) NonAssoc
-                )
-            )
-            [ TermVar
-                ( NamedVar "A" )
-            ]
-        ]
-    }
-, Task
-    { taskDirectness = Direct
-    , taskHypotheses =
-        [ Hypothesis Marker "fin_intro_ref" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 32
-                        , locColumn = 16
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 32
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 32
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "fin" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "fin" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    ]
-                )
-            )
-        , Hypothesis Marker "fin_intro_1" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 26
-                            , locColumn = 16
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    , TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "fin" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "fin" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    ]
-                )
-            )
-        , Hypothesis Marker "fin_intro_2" Quantified Universally
-            ( Scope
-                ( Connected Implication
-                    ( Connected Conjunction
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 20
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Command "in" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "elem" )
-                                    )
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "a" )
-                                )
-                            , TermVar
-                                ( B
-                                    ( NamedVar "A" )
-                                )
-                            ]
-                        )
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Command "in" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "elem" )
-                                    )
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "B" )
-                                )
-                            , TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolMixfix
-                                    ( MixfixItem
-                                        ( TokenCons
-                                            ( Command "fin" )
-                                            ( TokenCons InvisibleBraceL
-                                                ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                            )
-                                        )
-                                        ( Marker "fin" ) NonAssoc
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "A" )
-                                    )
-                                ]
-                            ]
-                        )
-                    )
-                    ( TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 52
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "cons" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons
-                                                ( TokenCons InvisibleBraceR
-                                                    ( TokenCons InvisibleBraceL
-                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                    )
-                                                )
-                                            )
-                                        )
-                                    )
-                                    ( Marker "cons" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "a" )
-                                )
-                            , TermVar
-                                ( B
-                                    ( NamedVar "B" )
-                                )
-                            ]
-                        , TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "fin" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "fin" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "A" )
-                                )
-                            ]
-                        ]
-                    )
-                )
-            )
-        , Hypothesis Marker "fin_dom_subset" Quantified Universally
-            ( Scope
-                ( Quantified Universally
-                    ( Scope
-                        ( Connected Implication
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x" )
-                                    )
-                                , TermSymbol
-                                    ( Location
-                                        { locFile = "<nowhere>"
-                                        , locLine = -1
-                                        , locColumn = -1
-                                        }
-                                    )
-                                    ( SymbolMixfix
-                                        ( MixfixItem
-                                            ( TokenCons
-                                                ( Command "fin" )
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                            ( Marker "fin" ) NonAssoc
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "A" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                ]
-                            )
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x" )
-                                    )
-                                , TermSymbol
-                                    ( Location
-                                        { locFile = "test/examples/inductive.tex"
-                                        , locLine = 24
-                                        , locColumn = 29
-                                        }
-                                    )
-                                    ( SymbolMixfix
-                                        ( MixfixItem
-                                            ( TokenCons
-                                                ( Command "pow" )
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                            ( Marker "pow" ) NonAssoc
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "A" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                ]
-                            )
-                        )
-                    )
-                )
-            )
-        , Hypothesis Marker "fin_cases" Quantified Universally
-            ( Scope
-                ( Connected Implication
-                    ( TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "x" )
-                            )
-                        , TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "fin" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "fin" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "A" )
-                                )
-                            ]
-                        ]
-                    )
-                    ( Connected Disjunction
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Symbol "=" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "eq" )
-                                    )
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "x" )
-                                )
-                            , TermSymbol
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 26
-                                    , locColumn = 16
-                                    }
-                                )
-                                ( SymbolMixfix
-                                    ( MixfixItem
-                                        ( TokenCons
-                                            ( Command "emptyset" ) End
-                                        )
-                                        ( Marker "emptyset" ) NonAssoc
-                                    )
-                                ) []
-                            ]
-                        )
-                        ( Quantified Existentially
-                            ( Scope
-                                ( Connected Conjunction
-                                    ( Connected Conjunction
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 20
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( F
-                                                    ( TermVar
-                                                        ( B
-                                                            ( NamedVar "A" )
-                                                        )
-                                                    )
-                                                )
-                                            ]
-                                        )
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "<nowhere>"
-                                                , locLine = -1
-                                                , locColumn = -1
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            , TermSymbol
-                                                ( Location
-                                                    { locFile = "<nowhere>"
-                                                    , locLine = -1
-                                                    , locColumn = -1
-                                                    }
-                                                )
-                                                ( SymbolMixfix
-                                                    ( MixfixItem
-                                                        ( TokenCons
-                                                            ( Command "fin" )
-                                                            ( TokenCons InvisibleBraceL
-                                                                ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                            )
-                                                        )
-                                                        ( Marker "fin" ) NonAssoc
-                                                    )
-                                                )
-                                                [ TermVar
-                                                    ( F
-                                                        ( TermVar
-                                                            ( B
-                                                                ( NamedVar "A" )
-                                                            )
-                                                        )
-                                                    )
-                                                ]
-                                            ]
-                                        )
-                                    )
-                                    ( TermSymbol
-                                        ( Location
-                                            { locFile = "<nowhere>"
-                                            , locLine = -1
-                                            , locColumn = -1
-                                            }
-                                        )
-                                        ( SymbolPredicate
-                                            ( PredicateRelation
-                                                ( RelationSymbol
-                                                    ( Symbol "=" )
-                                                    ( ParameterArity 0 )
-                                                    ( Marker "eq" )
-                                                )
-                                            )
-                                        )
-                                        [ TermVar
-                                            ( F
-                                                ( TermVar
-                                                    ( B
-                                                        ( NamedVar "x" )
-                                                    )
-                                                )
-                                            )
-                                        , TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 52
-                                                }
-                                            )
-                                            ( SymbolMixfix
-                                                ( MixfixItem
-                                                    ( TokenCons
-                                                        ( Command "cons" )
-                                                        ( TokenCons InvisibleBraceL
-                                                            ( HoleCons
-                                                                ( TokenCons InvisibleBraceR
-                                                                    ( TokenCons InvisibleBraceL
-                                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                                    )
-                                                                )
-                                                            )
-                                                        )
-                                                    )
-                                                    ( Marker "cons" ) NonAssoc
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            ]
-                                        ]
-                                    )
-                                )
-                            )
-                        )
-                    )
-                )
-            )
-        , Hypothesis Marker "fin_induct" Quantified Universally
-            ( Scope
-                ( Connected Implication
-                    ( Connected Conjunction
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Command "in" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "elem" )
-                                    )
-                                )
-                            )
-                            [ TermSymbol
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 26
-                                    , locColumn = 16
-                                    }
-                                )
-                                ( SymbolMixfix
-                                    ( MixfixItem
-                                        ( TokenCons
-                                            ( Command "emptyset" ) End
-                                        )
-                                        ( Marker "emptyset" ) NonAssoc
-                                    )
-                                ) []
-                            , TermVar
-                                ( B
-                                    ( NamedVar "S" )
-                                )
-                            ]
-                        )
-                        ( Quantified Universally
-                            ( Scope
-                                ( Connected Implication
-                                    ( Connected Conjunction
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 20
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( F
-                                                    ( TermVar
-                                                        ( B
-                                                            ( NamedVar "A" )
-                                                        )
-                                                    )
-                                                )
-                                            ]
-                                        )
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "<nowhere>"
-                                                , locLine = -1
-                                                , locColumn = -1
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            , TermVar
-                                                ( F
-                                                    ( TermVar
-                                                        ( B
-                                                            ( NamedVar "S" )
-                                                        )
-                                                    )
-                                                )
-                                            ]
-                                        )
-                                    )
-                                    ( TermSymbol
-                                        ( Location
-                                            { locFile = "<nowhere>"
-                                            , locLine = -1
-                                            , locColumn = -1
-                                            }
-                                        )
-                                        ( SymbolPredicate
-                                            ( PredicateRelation
-                                                ( RelationSymbol
-                                                    ( Command "in" )
-                                                    ( ParameterArity 0 )
-                                                    ( Marker "elem" )
-                                                )
-                                            )
-                                        )
-                                        [ TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 52
-                                                }
-                                            )
-                                            ( SymbolMixfix
-                                                ( MixfixItem
-                                                    ( TokenCons
-                                                        ( Command "cons" )
-                                                        ( TokenCons InvisibleBraceL
-                                                            ( HoleCons
-                                                                ( TokenCons InvisibleBraceR
-                                                                    ( TokenCons InvisibleBraceL
-                                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                                    )
-                                                                )
-                                                            )
-                                                        )
-                                                    )
-                                                    ( Marker "cons" ) NonAssoc
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            ]
-                                        , TermVar
-                                            ( F
-                                                ( TermVar
-                                                    ( B
-                                                        ( NamedVar "S" )
-                                                    )
-                                                )
-                                            )
-                                        ]
-                                    )
-                                )
-                            )
-                        )
-                    )
-                    ( Quantified Universally
-                        ( Scope
-                            ( Connected Implication
-                                ( TermSymbol
-                                    ( Location
-                                        { locFile = "<nowhere>"
-                                        , locLine = -1
-                                        , locColumn = -1
-                                        }
-                                    )
-                                    ( SymbolPredicate
-                                        ( PredicateRelation
-                                            ( RelationSymbol
-                                                ( Command "in" )
-                                                ( ParameterArity 0 )
-                                                ( Marker "elem" )
-                                            )
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( B
-                                            ( NamedVar "x" )
-                                        )
-                                    , TermSymbol
-                                        ( Location
-                                            { locFile = "<nowhere>"
-                                            , locLine = -1
-                                            , locColumn = -1
-                                            }
-                                        )
-                                        ( SymbolMixfix
-                                            ( MixfixItem
-                                                ( TokenCons
-                                                    ( Command "fin" )
-                                                    ( TokenCons InvisibleBraceL
-                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                    )
-                                                )
-                                                ( Marker "fin" ) NonAssoc
-                                            )
-                                        )
-                                        [ TermVar
-                                            ( F
-                                                ( TermVar
-                                                    ( B
-                                                        ( NamedVar "A" )
-                                                    )
-                                                )
-                                            )
-                                        ]
-                                    ]
-                                )
-                                ( TermSymbol
-                                    ( Location
-                                        { locFile = "<nowhere>"
-                                        , locLine = -1
-                                        , locColumn = -1
-                                        }
-                                    )
-                                    ( SymbolPredicate
-                                        ( PredicateRelation
-                                            ( RelationSymbol
-                                                ( Command "in" )
-                                                ( ParameterArity 0 )
-                                                ( Marker "elem" )
-                                            )
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( B
-                                            ( NamedVar "x" )
-                                        )
-                                    , TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "S" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                )
-                            )
-                        )
-                    )
-                )
-            )
-        , Hypothesis Marker "everything_in_emptyset" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 20
-                        , locColumn = 7
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermVar
-                        ( B
-                            ( NamedVar "x" )
-                        )
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 20
-                            , locColumn = 10
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "wrap" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 16
-                            , locColumn = 17
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "cons" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 12
-                        , locColumn = 18
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "cons" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons
-                                            ( TokenCons InvisibleBraceR
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                        )
-                                    )
-                                )
-                                ( Marker "cons" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "a" )
-                            )
-                        , TermVar
-                            ( B
-                                ( NamedVar "B" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "pow" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 8
-                        , locColumn = 14
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "pow" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "pow" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 16
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        ]
-    , taskConjectureLabel = Marker "acc"
-    , taskLocation = Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 38
-        , locColumn = 1
-        }
-    , taskConjecture = Quantified Universally
-        ( Scope
-            ( Connected Implication
-                ( Quantified Universally
-                    ( Scope
-                        ( Connected Implication
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x1" )
-                                    )
-                                , TermVar
-                                    ( F
-                                        ( TermVar
-                                            ( B
-                                                ( NamedVar "xa" )
-                                            )
-                                        )
-                                    )
-                                ]
-                            )
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x1" )
-                                    )
-                                , TermVar
-                                    ( F
-                                        ( TermVar
-                                            ( B
-                                                ( NamedVar "xb" )
-                                            )
-                                        )
-                                    )
-                                ]
-                            )
-                        )
-                    )
-                )
-                ( Quantified Universally
-                    ( Scope
-                        ( Connected Implication
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x1" )
-                                    )
-                                , TermSymbol
-                                    ( Location
-                                        { locFile = "test/examples/inductive.tex"
-                                        , locLine = 41
-                                        , locColumn = 23
-                                        }
-                                    )
-                                    ( SymbolMixfix
-                                        ( MixfixItem
-                                            ( TokenCons
-                                                ( Command "wrap" )
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                            ( Marker "wrap" ) NonAssoc
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "xa" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                ]
-                            )
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x1" )
-                                    )
-                                , TermSymbol
-                                    ( Location
-                                        { locFile = "test/examples/inductive.tex"
-                                        , locLine = 41
-                                        , locColumn = 23
-                                        }
-                                    )
-                                    ( SymbolMixfix
-                                        ( MixfixItem
-                                            ( TokenCons
-                                                ( Command "wrap" )
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                            ( Marker "wrap" ) NonAssoc
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "xb" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                ]
-                            )
-                        )
-                    )
-                )
-            )
-        )
-    }
-, Task
-    { taskDirectness = Direct
-    , taskHypotheses =
-        [ Hypothesis Marker "fin_intro_ref" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 32
-                        , locColumn = 16
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 32
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 32
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "fin" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "fin" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    ]
-                )
-            )
-        , Hypothesis Marker "fin_intro_1" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 26
-                            , locColumn = 16
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    , TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "fin" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "fin" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    ]
-                )
-            )
-        , Hypothesis Marker "fin_intro_2" Quantified Universally
-            ( Scope
-                ( Connected Implication
-                    ( Connected Conjunction
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 20
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Command "in" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "elem" )
-                                    )
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "a" )
-                                )
-                            , TermVar
-                                ( B
-                                    ( NamedVar "A" )
-                                )
-                            ]
-                        )
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Command "in" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "elem" )
-                                    )
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "B" )
-                                )
-                            , TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolMixfix
-                                    ( MixfixItem
-                                        ( TokenCons
-                                            ( Command "fin" )
-                                            ( TokenCons InvisibleBraceL
-                                                ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                            )
-                                        )
-                                        ( Marker "fin" ) NonAssoc
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "A" )
-                                    )
-                                ]
-                            ]
-                        )
-                    )
-                    ( TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 52
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "cons" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons
-                                                ( TokenCons InvisibleBraceR
-                                                    ( TokenCons InvisibleBraceL
-                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                    )
-                                                )
-                                            )
-                                        )
-                                    )
-                                    ( Marker "cons" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "a" )
-                                )
-                            , TermVar
-                                ( B
-                                    ( NamedVar "B" )
-                                )
-                            ]
-                        , TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "fin" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "fin" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "A" )
-                                )
-                            ]
-                        ]
-                    )
-                )
-            )
-        , Hypothesis Marker "fin_dom_subset" Quantified Universally
-            ( Scope
-                ( Quantified Universally
-                    ( Scope
-                        ( Connected Implication
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x" )
-                                    )
-                                , TermSymbol
-                                    ( Location
-                                        { locFile = "<nowhere>"
-                                        , locLine = -1
-                                        , locColumn = -1
-                                        }
-                                    )
-                                    ( SymbolMixfix
-                                        ( MixfixItem
-                                            ( TokenCons
-                                                ( Command "fin" )
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                            ( Marker "fin" ) NonAssoc
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "A" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                ]
-                            )
-                            ( TermSymbol
-                                ( Location
-                                    { locFile = "<nowhere>"
-                                    , locLine = -1
-                                    , locColumn = -1
-                                    }
-                                )
-                                ( SymbolPredicate
-                                    ( PredicateRelation
-                                        ( RelationSymbol
-                                            ( Command "in" )
-                                            ( ParameterArity 0 )
-                                            ( Marker "elem" )
-                                        )
-                                    )
-                                )
-                                [ TermVar
-                                    ( B
-                                        ( NamedVar "x" )
-                                    )
-                                , TermSymbol
-                                    ( Location
-                                        { locFile = "test/examples/inductive.tex"
-                                        , locLine = 24
-                                        , locColumn = 29
-                                        }
-                                    )
-                                    ( SymbolMixfix
-                                        ( MixfixItem
-                                            ( TokenCons
-                                                ( Command "pow" )
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                            ( Marker "pow" ) NonAssoc
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "A" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                ]
-                            )
-                        )
-                    )
-                )
-            )
-        , Hypothesis Marker "fin_cases" Quantified Universally
-            ( Scope
-                ( Connected Implication
-                    ( TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "x" )
-                            )
-                        , TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "fin" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "fin" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "A" )
-                                )
-                            ]
-                        ]
-                    )
-                    ( Connected Disjunction
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Symbol "=" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "eq" )
-                                    )
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "x" )
-                                )
-                            , TermSymbol
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 26
-                                    , locColumn = 16
-                                    }
-                                )
-                                ( SymbolMixfix
-                                    ( MixfixItem
-                                        ( TokenCons
-                                            ( Command "emptyset" ) End
-                                        )
-                                        ( Marker "emptyset" ) NonAssoc
-                                    )
-                                ) []
-                            ]
-                        )
-                        ( Quantified Existentially
-                            ( Scope
-                                ( Connected Conjunction
-                                    ( Connected Conjunction
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 20
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( F
-                                                    ( TermVar
-                                                        ( B
-                                                            ( NamedVar "A" )
-                                                        )
-                                                    )
-                                                )
-                                            ]
-                                        )
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "<nowhere>"
-                                                , locLine = -1
-                                                , locColumn = -1
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            , TermSymbol
-                                                ( Location
-                                                    { locFile = "<nowhere>"
-                                                    , locLine = -1
-                                                    , locColumn = -1
-                                                    }
-                                                )
-                                                ( SymbolMixfix
-                                                    ( MixfixItem
-                                                        ( TokenCons
-                                                            ( Command "fin" )
-                                                            ( TokenCons InvisibleBraceL
-                                                                ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                            )
-                                                        )
-                                                        ( Marker "fin" ) NonAssoc
-                                                    )
-                                                )
-                                                [ TermVar
-                                                    ( F
-                                                        ( TermVar
-                                                            ( B
-                                                                ( NamedVar "A" )
-                                                            )
-                                                        )
-                                                    )
-                                                ]
-                                            ]
-                                        )
-                                    )
-                                    ( TermSymbol
-                                        ( Location
-                                            { locFile = "<nowhere>"
-                                            , locLine = -1
-                                            , locColumn = -1
-                                            }
-                                        )
-                                        ( SymbolPredicate
-                                            ( PredicateRelation
-                                                ( RelationSymbol
-                                                    ( Symbol "=" )
-                                                    ( ParameterArity 0 )
-                                                    ( Marker "eq" )
-                                                )
-                                            )
-                                        )
-                                        [ TermVar
-                                            ( F
-                                                ( TermVar
-                                                    ( B
-                                                        ( NamedVar "x" )
-                                                    )
-                                                )
-                                            )
-                                        , TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 52
-                                                }
-                                            )
-                                            ( SymbolMixfix
-                                                ( MixfixItem
-                                                    ( TokenCons
-                                                        ( Command "cons" )
-                                                        ( TokenCons InvisibleBraceL
-                                                            ( HoleCons
-                                                                ( TokenCons InvisibleBraceR
-                                                                    ( TokenCons InvisibleBraceL
-                                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                                    )
-                                                                )
-                                                            )
-                                                        )
-                                                    )
-                                                    ( Marker "cons" ) NonAssoc
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            ]
-                                        ]
-                                    )
-                                )
-                            )
-                        )
-                    )
-                )
-            )
-        , Hypothesis Marker "fin_induct" Quantified Universally
-            ( Scope
-                ( Connected Implication
-                    ( Connected Conjunction
-                        ( TermSymbol
-                            ( Location
-                                { locFile = "<nowhere>"
-                                , locLine = -1
-                                , locColumn = -1
-                                }
-                            )
-                            ( SymbolPredicate
-                                ( PredicateRelation
-                                    ( RelationSymbol
-                                        ( Command "in" )
-                                        ( ParameterArity 0 )
-                                        ( Marker "elem" )
-                                    )
-                                )
-                            )
-                            [ TermSymbol
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 26
-                                    , locColumn = 16
-                                    }
-                                )
-                                ( SymbolMixfix
-                                    ( MixfixItem
-                                        ( TokenCons
-                                            ( Command "emptyset" ) End
-                                        )
-                                        ( Marker "emptyset" ) NonAssoc
-                                    )
-                                ) []
-                            , TermVar
-                                ( B
-                                    ( NamedVar "S" )
-                                )
-                            ]
-                        )
-                        ( Quantified Universally
-                            ( Scope
-                                ( Connected Implication
-                                    ( Connected Conjunction
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 20
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( F
-                                                    ( TermVar
-                                                        ( B
-                                                            ( NamedVar "A" )
-                                                        )
-                                                    )
-                                                )
-                                            ]
-                                        )
-                                        ( TermSymbol
-                                            ( Location
-                                                { locFile = "<nowhere>"
-                                                , locLine = -1
-                                                , locColumn = -1
-                                                }
-                                            )
-                                            ( SymbolPredicate
-                                                ( PredicateRelation
-                                                    ( RelationSymbol
-                                                        ( Command "in" )
-                                                        ( ParameterArity 0 )
-                                                        ( Marker "elem" )
-                                                    )
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            , TermVar
-                                                ( F
-                                                    ( TermVar
-                                                        ( B
-                                                            ( NamedVar "S" )
-                                                        )
-                                                    )
-                                                )
-                                            ]
-                                        )
-                                    )
-                                    ( TermSymbol
-                                        ( Location
-                                            { locFile = "<nowhere>"
-                                            , locLine = -1
-                                            , locColumn = -1
-                                            }
-                                        )
-                                        ( SymbolPredicate
-                                            ( PredicateRelation
-                                                ( RelationSymbol
-                                                    ( Command "in" )
-                                                    ( ParameterArity 0 )
-                                                    ( Marker "elem" )
-                                                )
-                                            )
-                                        )
-                                        [ TermSymbol
-                                            ( Location
-                                                { locFile = "test/examples/inductive.tex"
-                                                , locLine = 27
-                                                , locColumn = 52
-                                                }
-                                            )
-                                            ( SymbolMixfix
-                                                ( MixfixItem
-                                                    ( TokenCons
-                                                        ( Command "cons" )
-                                                        ( TokenCons InvisibleBraceL
-                                                            ( HoleCons
-                                                                ( TokenCons InvisibleBraceR
-                                                                    ( TokenCons InvisibleBraceL
-                                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                                    )
-                                                                )
-                                                            )
-                                                        )
-                                                    )
-                                                    ( Marker "cons" ) NonAssoc
-                                                )
-                                            )
-                                            [ TermVar
-                                                ( B
-                                                    ( NamedVar "a" )
-                                                )
-                                            , TermVar
-                                                ( B
-                                                    ( NamedVar "B" )
-                                                )
-                                            ]
-                                        , TermVar
-                                            ( F
-                                                ( TermVar
-                                                    ( B
-                                                        ( NamedVar "S" )
-                                                    )
-                                                )
-                                            )
-                                        ]
-                                    )
-                                )
-                            )
-                        )
-                    )
-                    ( Quantified Universally
-                        ( Scope
-                            ( Connected Implication
-                                ( TermSymbol
-                                    ( Location
-                                        { locFile = "<nowhere>"
-                                        , locLine = -1
-                                        , locColumn = -1
-                                        }
-                                    )
-                                    ( SymbolPredicate
-                                        ( PredicateRelation
-                                            ( RelationSymbol
-                                                ( Command "in" )
-                                                ( ParameterArity 0 )
-                                                ( Marker "elem" )
-                                            )
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( B
-                                            ( NamedVar "x" )
-                                        )
-                                    , TermSymbol
-                                        ( Location
-                                            { locFile = "<nowhere>"
-                                            , locLine = -1
-                                            , locColumn = -1
-                                            }
-                                        )
-                                        ( SymbolMixfix
-                                            ( MixfixItem
-                                                ( TokenCons
-                                                    ( Command "fin" )
-                                                    ( TokenCons InvisibleBraceL
-                                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                    )
-                                                )
-                                                ( Marker "fin" ) NonAssoc
-                                            )
-                                        )
-                                        [ TermVar
-                                            ( F
-                                                ( TermVar
-                                                    ( B
-                                                        ( NamedVar "A" )
-                                                    )
-                                                )
-                                            )
-                                        ]
-                                    ]
-                                )
-                                ( TermSymbol
-                                    ( Location
-                                        { locFile = "<nowhere>"
-                                        , locLine = -1
-                                        , locColumn = -1
-                                        }
-                                    )
-                                    ( SymbolPredicate
-                                        ( PredicateRelation
-                                            ( RelationSymbol
-                                                ( Command "in" )
-                                                ( ParameterArity 0 )
-                                                ( Marker "elem" )
-                                            )
-                                        )
-                                    )
-                                    [ TermVar
-                                        ( B
-                                            ( NamedVar "x" )
-                                        )
-                                    , TermVar
-                                        ( F
-                                            ( TermVar
-                                                ( B
-                                                    ( NamedVar "S" )
-                                                )
-                                            )
-                                        )
-                                    ]
-                                )
-                            )
-                        )
-                    )
-                )
-            )
-        , Hypothesis Marker "everything_in_emptyset" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 20
-                        , locColumn = 7
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermVar
-                        ( B
-                            ( NamedVar "x" )
-                        )
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 20
-                            , locColumn = 10
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "wrap" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "<nowhere>"
-                            , locLine = -1
-                            , locColumn = -1
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 16
-                            , locColumn = 17
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "cons" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 12
-                        , locColumn = 18
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "cons" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons
-                                            ( TokenCons InvisibleBraceR
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                        )
-                                    )
-                                )
-                                ( Marker "cons" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "a" )
-                            )
-                        , TermVar
-                            ( B
-                                ( NamedVar "B" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        , Hypothesis Marker "pow" Quantified Universally
-            ( Scope
-                ( TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 8
-                        , locColumn = 14
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Symbol "=" )
-                                ( ParameterArity 0 )
-                                ( Marker "eq" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 6
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "pow" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "pow" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "A" )
-                            )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 16
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "emptyset" ) End
-                                )
-                                ( Marker "emptyset" ) NonAssoc
-                            )
-                        ) []
-                    ]
-                )
-            )
-        ]
-    , taskConjectureLabel = Marker "acc"
-    , taskLocation = Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 38
-        , locColumn = 1
-        }
-    , taskConjecture = Quantified Universally
-        ( Scope
-            ( Connected Implication
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermVar
-                        ( B
-                            ( NamedVar "x" )
-                        )
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 41
-                            , locColumn = 23
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                        )
-                        [ TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 39
-                                , locColumn = 29
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "wrap" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "wrap" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( B
-                                    ( NamedVar "R" )
-                                )
-                            ]
-                        ]
-                    ]
-                )
-                ( TermSymbol
-                    ( Location
-                        { locFile = "<nowhere>"
-                        , locLine = -1
-                        , locColumn = -1
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermVar
-                        ( B
-                            ( NamedVar "x" )
-                        )
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 39
-                            , locColumn = 29
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( B
-                                ( NamedVar "R" )
-                            )
-                        ]
-                    ]
-                )
-            )
-        )
-    }
 ]
\ No newline at end of file
diff --git a/test/golden/inductive/glossing.golden b/test/golden/inductive/glossing.golden
index 57892a3..98f60e8 100644
--- a/test/golden/inductive/glossing.golden
+++ b/test/golden/inductive/glossing.golden
@@ -1,224 +1,7 @@
-[ BlockAxiom
+[ BlockInductive
     ( Location
         { locFile = "test/examples/inductive.tex"
-        , locLine = 7
-        , locColumn = 1
-        }
-    )
-    ( Marker "pow" )
-    ( Axiom []
-        ( TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 8
-                , locColumn = 14
-                }
-            )
-            ( SymbolPredicate
-                ( PredicateRelation
-                    ( RelationSymbol
-                        ( Symbol "=" )
-                        ( ParameterArity 0 )
-                        ( Marker "eq" )
-                    )
-                )
-            )
-            [ TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 8
-                    , locColumn = 6
-                    }
-                )
-                ( SymbolMixfix
-                    ( MixfixItem
-                        ( TokenCons
-                            ( Command "pow" )
-                            ( TokenCons InvisibleBraceL
-                                ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                            )
-                        )
-                        ( Marker "pow" ) NonAssoc
-                    )
-                )
-                [ TermVar
-                    ( NamedVar "A" )
-                ]
-            , TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 8
-                    , locColumn = 16
-                    }
-                )
-                ( SymbolMixfix
-                    ( MixfixItem
-                        ( TokenCons
-                            ( Command "emptyset" ) End
-                        )
-                        ( Marker "emptyset" ) NonAssoc
-                    )
-                ) []
-            ]
-        )
-    )
-, BlockAxiom
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 11
-        , locColumn = 1
-        }
-    )
-    ( Marker "cons" )
-    ( Axiom []
-        ( TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 12
-                , locColumn = 18
-                }
-            )
-            ( SymbolPredicate
-                ( PredicateRelation
-                    ( RelationSymbol
-                        ( Symbol "=" )
-                        ( ParameterArity 0 )
-                        ( Marker "eq" )
-                    )
-                )
-            )
-            [ TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 12
-                    , locColumn = 6
-                    }
-                )
-                ( SymbolMixfix
-                    ( MixfixItem
-                        ( TokenCons
-                            ( Command "cons" )
-                            ( TokenCons InvisibleBraceL
-                                ( HoleCons
-                                    ( TokenCons InvisibleBraceR
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                )
-                            )
-                        )
-                        ( Marker "cons" ) NonAssoc
-                    )
-                )
-                [ TermVar
-                    ( NamedVar "a" )
-                , TermVar
-                    ( NamedVar "B" )
-                ]
-            , TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 12
-                    , locColumn = 20
-                    }
-                )
-                ( SymbolMixfix
-                    ( MixfixItem
-                        ( TokenCons
-                            ( Command "emptyset" ) End
-                        )
-                        ( Marker "emptyset" ) NonAssoc
-                    )
-                ) []
-            ]
-        )
-    )
-, BlockDefn
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 15
-        , locColumn = 1
-        }
-    )
-    ( Marker "wrap" )
-    ( DefnOp
-        ( MixfixItem
-            ( TokenCons
-                ( Command "wrap" )
-                ( TokenCons InvisibleBraceL
-                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                )
-            )
-            ( Marker "wrap" ) NonAssoc
-        )
-        [ NamedVar "A" ]
-        ( TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 16
-                , locColumn = 17
-                }
-            )
-            ( SymbolMixfix
-                ( MixfixItem
-                    ( TokenCons
-                        ( Command "emptyset" ) End
-                    )
-                    ( Marker "emptyset" ) NonAssoc
-                )
-            ) []
-        )
-    )
-, BlockAxiom
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 19
-        , locColumn = 1
-        }
-    )
-    ( Marker "everything_in_emptyset" )
-    ( Axiom []
-        ( TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 20
-                , locColumn = 7
-                }
-            )
-            ( SymbolPredicate
-                ( PredicateRelation
-                    ( RelationSymbol
-                        ( Command "in" )
-                        ( ParameterArity 0 )
-                        ( Marker "elem" )
-                    )
-                )
-            )
-            [ TermVar
-                ( NamedVar "x" )
-            , TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 20
-                    , locColumn = 10
-                    }
-                )
-                ( SymbolMixfix
-                    ( MixfixItem
-                        ( TokenCons
-                            ( Command "emptyset" ) End
-                        )
-                        ( Marker "emptyset" ) NonAssoc
-                    )
-                ) []
-            ]
-        )
-    )
-, BlockInductive
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 23
+        , locLine = 3
         , locColumn = 1
         }
     )
@@ -237,19 +20,19 @@
         , inductiveDomain = TermSymbol
             ( Location
                 { locFile = "test/examples/inductive.tex"
-                , locLine = 24
+                , locLine = 4
                 , locColumn = 29
                 }
             )
             ( SymbolMixfix
                 ( MixfixItem
                     ( TokenCons
-                        ( Command "pow" )
+                        ( Command "cumul" )
                         ( TokenCons InvisibleBraceL
                             ( HoleCons ( TokenCons InvisibleBraceR End ) )
                         )
                     )
-                    ( Marker "pow" ) NonAssoc
+                    ( Marker "cumul" ) NonAssoc
                 )
             )
             [ TermVar
@@ -260,8 +43,8 @@
             , introResult = TermSymbol
                 ( Location
                     { locFile = "test/examples/inductive.tex"
-                    , locLine = 26
-                    , locColumn = 26
+                    , locLine = 6
+                    , locColumn = 17
                     }
                 )
                 ( SymbolPredicate
@@ -273,26 +56,13 @@
                         )
                     )
                 )
-                [ TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 26
-                        , locColumn = 16
-                        }
-                    )
-                    ( SymbolMixfix
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "emptyset" ) End
-                            )
-                            ( Marker "emptyset" ) NonAssoc
-                        )
-                    ) []
+                [ TermVar
+                    ( NamedVar "A" )
                 , TermSymbol
                     ( Location
                         { locFile = "test/examples/inductive.tex"
-                        , locLine = 26
-                        , locColumn = 29
+                        , locLine = 6
+                        , locColumn = 20
                         }
                     )
                     ( SymbolMixfix
@@ -310,373 +80,6 @@
                         ( NamedVar "A" )
                     ]
                 ]
-            } :|
-            [ IntroRule
-                { introConditions =
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 27
-                            , locColumn = 20
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermVar
-                            ( NamedVar "a" )
-                        , TermVar
-                            ( NamedVar "A" )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 27
-                            , locColumn = 33
-                            }
-                        )
-                        ( SymbolPredicate
-                            ( PredicateRelation
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                )
-                            )
-                        )
-                        [ TermVar
-                            ( NamedVar "B" )
-                        , TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 36
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "fin" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "fin" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( NamedVar "A" )
-                            ]
-                        ]
-                    ]
-                , introResult = TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 27
-                        , locColumn = 63
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 27
-                            , locColumn = 52
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "cons" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons
-                                            ( TokenCons InvisibleBraceR
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                        )
-                                    )
-                                )
-                                ( Marker "cons" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( NamedVar "a" )
-                        , TermVar
-                            ( NamedVar "B" )
-                        ]
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 27
-                            , locColumn = 66
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "fin" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "fin" ) NonAssoc
-                            )
-                        )
-                        [ TermVar
-                            ( NamedVar "A" )
-                        ]
-                    ]
-                }
-            ]
-        }
-    )
-, BlockLemma
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 31
-        , locColumn = 1
-        }
-    )
-    ( Marker "fin_intro_ref" )
-    ( Lemma []
-        ( TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 32
-                , locColumn = 16
-                }
-            )
-            ( SymbolPredicate
-                ( PredicateRelation
-                    ( RelationSymbol
-                        ( Command "in" )
-                        ( ParameterArity 0 )
-                        ( Marker "elem" )
-                    )
-                )
-            )
-            [ TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 32
-                    , locColumn = 6
-                    }
-                )
-                ( SymbolMixfix
-                    ( MixfixItem
-                        ( TokenCons
-                            ( Command "emptyset" ) End
-                        )
-                        ( Marker "emptyset" ) NonAssoc
-                    )
-                ) []
-            , TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 32
-                    , locColumn = 20
-                    }
-                )
-                ( SymbolMixfix
-                    ( MixfixItem
-                        ( TokenCons
-                            ( Command "fin" )
-                            ( TokenCons InvisibleBraceL
-                                ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                            )
-                        )
-                        ( Marker "fin" ) NonAssoc
-                    )
-                )
-                [ TermVar
-                    ( NamedVar "A" )
-                ]
-            ]
-        )
-    )
-, BlockProof
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 34
-        , locColumn = 1
-        }
-    )
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 36
-        , locColumn = 1
-        }
-    )
-    ( Qed
-        { mloc = Just
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 35
-                , locColumn = 5
-                }
-            )
-        , by = JustificationRef
-            ( Marker "fin_intro_1" :| [] )
-        }
-    )
-, BlockInductive
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 38
-        , locColumn = 1
-        }
-    )
-    ( Marker "acc" )
-    ( Inductive
-        { inductiveSymbol = MixfixItem
-            ( TokenCons
-                ( Command "acc" )
-                ( TokenCons InvisibleBraceL
-                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                )
-            )
-            ( Marker "acc" ) NonAssoc
-        , inductiveParams =
-            [ NamedVar "R" ]
-        , inductiveDomain = TermSymbol
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 39
-                , locColumn = 29
-                }
-            )
-            ( SymbolMixfix
-                ( MixfixItem
-                    ( TokenCons
-                        ( Command "wrap" )
-                        ( TokenCons InvisibleBraceL
-                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                        )
-                    )
-                    ( Marker "wrap" ) NonAssoc
-                )
-            )
-            [ TermVar
-                ( NamedVar "R" )
-            ]
-        , inductiveIntros = IntroRule
-            { introConditions =
-                [ TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 41
-                        , locColumn = 20
-                        }
-                    )
-                    ( SymbolPredicate
-                        ( PredicateRelation
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            )
-                        )
-                    )
-                    [ TermVar
-                        ( NamedVar "x" )
-                    , TermSymbol
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 41
-                            , locColumn = 23
-                            }
-                        )
-                        ( SymbolMixfix
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                        )
-                        [ TermSymbol
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 41
-                                , locColumn = 29
-                                }
-                            )
-                            ( SymbolMixfix
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "acc" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "acc" ) NonAssoc
-                                )
-                            )
-                            [ TermVar
-                                ( NamedVar "R" )
-                            ]
-                        ]
-                    ]
-                ]
-            , introResult = TermSymbol
-                ( Location
-                    { locFile = "test/examples/inductive.tex"
-                    , locLine = 41
-                    , locColumn = 47
-                    }
-                )
-                ( SymbolPredicate
-                    ( PredicateRelation
-                        ( RelationSymbol
-                            ( Command "in" )
-                            ( ParameterArity 0 )
-                            ( Marker "elem" )
-                        )
-                    )
-                )
-                [ TermVar
-                    ( NamedVar "x" )
-                , TermSymbol
-                    ( Location
-                        { locFile = "test/examples/inductive.tex"
-                        , locLine = 41
-                        , locColumn = 50
-                        }
-                    )
-                    ( SymbolMixfix
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "acc" )
-                                ( TokenCons InvisibleBraceL
-                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                )
-                            )
-                            ( Marker "acc" ) NonAssoc
-                        )
-                    )
-                    [ TermVar
-                        ( NamedVar "R" )
-                    ]
-                ]
             } :| []
         }
     )
diff --git a/test/golden/inductive/parsing.golden b/test/golden/inductive/parsing.golden
index b57a39f..e4492ae 100644
--- a/test/golden/inductive/parsing.golden
+++ b/test/golden/inductive/parsing.golden
@@ -1,223 +1,7 @@
-[ BlockAxiom
+[ BlockInductive
     ( Location
         { locFile = "test/examples/inductive.tex"
-        , locLine = 7
-        , locColumn = 1
-        }
-    ) Nothing
-    ( Marker "pow" )
-    ( Axiom []
-        ( StmtFormula
-            { formula = FormulaChain
-                ( ChainBase
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 6
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "pow" )
-                                ( TokenCons InvisibleBraceL
-                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                )
-                            )
-                            ( Marker "pow" ) NonAssoc
-                        )
-                        [ ExprVar
-                            ( NamedVar "A" )
-                        ] :| []
-                    ) Positive
-                    ( Relation
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 14
-                            }
-                        )
-                        ( RelationSymbol
-                            ( Symbol "=" )
-                            ( ParameterArity 0 )
-                            ( Marker "eq" )
-                        ) []
-                    )
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 8
-                            , locColumn = 16
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "emptyset" ) End
-                            )
-                            ( Marker "emptyset" ) NonAssoc
-                        ) [] :| []
-                    )
-                )
-            }
-        )
-    )
-, BlockAxiom
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 11
-        , locColumn = 1
-        }
-    ) Nothing
-    ( Marker "cons" )
-    ( Axiom []
-        ( StmtFormula
-            { formula = FormulaChain
-                ( ChainBase
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 6
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "cons" )
-                                ( TokenCons InvisibleBraceL
-                                    ( HoleCons
-                                        ( TokenCons InvisibleBraceR
-                                            ( TokenCons InvisibleBraceL
-                                                ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                            )
-                                        )
-                                    )
-                                )
-                            )
-                            ( Marker "cons" ) NonAssoc
-                        )
-                        [ ExprVar
-                            ( NamedVar "a" )
-                        , ExprVar
-                            ( NamedVar "B" )
-                        ] :| []
-                    ) Positive
-                    ( Relation
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 18
-                            }
-                        )
-                        ( RelationSymbol
-                            ( Symbol "=" )
-                            ( ParameterArity 0 )
-                            ( Marker "eq" )
-                        ) []
-                    )
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 12
-                            , locColumn = 20
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "emptyset" ) End
-                            )
-                            ( Marker "emptyset" ) NonAssoc
-                        ) [] :| []
-                    )
-                )
-            }
-        )
-    )
-, BlockDefn
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 15
-        , locColumn = 1
-        }
-    ) Nothing
-    ( Marker "wrap" )
-    ( DefnOp
-        ( SymbolPattern
-            ( MixfixItem
-                ( TokenCons
-                    ( Command "wrap" )
-                    ( TokenCons InvisibleBraceL
-                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                    )
-                )
-                ( Marker "wrap" ) NonAssoc
-            )
-            [ NamedVar "A" ]
-        )
-        ( ExprOp
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 16
-                , locColumn = 17
-                }
-            )
-            ( MixfixItem
-                ( TokenCons
-                    ( Command "emptyset" ) End
-                )
-                ( Marker "emptyset" ) NonAssoc
-            ) []
-        )
-    )
-, BlockAxiom
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 19
-        , locColumn = 1
-        }
-    ) Nothing
-    ( Marker "everything_in_emptyset" )
-    ( Axiom []
-        ( StmtFormula
-            { formula = FormulaChain
-                ( ChainBase
-                    ( ExprVar
-                        ( NamedVar "x" ) :| []
-                    ) Positive
-                    ( Relation
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 20
-                            , locColumn = 7
-                            }
-                        )
-                        ( RelationSymbol
-                            ( Command "in" )
-                            ( ParameterArity 0 )
-                            ( Marker "elem" )
-                        ) []
-                    )
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 20
-                            , locColumn = 10
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "emptyset" ) End
-                            )
-                            ( Marker "emptyset" ) NonAssoc
-                        ) [] :| []
-                    )
-                )
-            }
-        )
-    )
-, BlockInductive
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 23
+        , locLine = 3
         , locColumn = 1
         }
     ) Nothing
@@ -237,18 +21,18 @@
         , inductiveDomain = ExprOp
             ( Location
                 { locFile = "test/examples/inductive.tex"
-                , locLine = 24
+                , locLine = 4
                 , locColumn = 29
                 }
             )
             ( MixfixItem
                 ( TokenCons
-                    ( Command "pow" )
+                    ( Command "cumul" )
                     ( TokenCons InvisibleBraceL
                         ( HoleCons ( TokenCons InvisibleBraceR End ) )
                     )
                 )
-                ( Marker "pow" ) NonAssoc
+                ( Marker "cumul" ) NonAssoc
             )
             [ ExprVar
                 ( NamedVar "A" )
@@ -257,218 +41,14 @@
             { introConditions = []
             , introResult = FormulaChain
                 ( ChainBase
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 26
-                            , locColumn = 16
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "emptyset" ) End
-                            )
-                            ( Marker "emptyset" ) NonAssoc
-                        ) [] :| []
-                    ) Positive
-                    ( Relation
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 26
-                            , locColumn = 26
-                            }
-                        )
-                        ( RelationSymbol
-                            ( Command "in" )
-                            ( ParameterArity 0 )
-                            ( Marker "elem" )
-                        ) []
-                    )
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 26
-                            , locColumn = 29
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "fin" )
-                                ( TokenCons InvisibleBraceL
-                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                )
-                            )
-                            ( Marker "fin" ) NonAssoc
-                        )
-                        [ ExprVar
-                            ( NamedVar "A" )
-                        ] :| []
-                    )
-                )
-            } :|
-            [ IntroRule
-                { introConditions =
-                    [ FormulaChain
-                        ( ChainBase
-                            ( ExprVar
-                                ( NamedVar "a" ) :| []
-                            ) Positive
-                            ( Relation
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 27
-                                    , locColumn = 20
-                                    }
-                                )
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                ) []
-                            )
-                            ( ExprVar
-                                ( NamedVar "A" ) :| []
-                            )
-                        )
-                    , FormulaChain
-                        ( ChainBase
-                            ( ExprVar
-                                ( NamedVar "B" ) :| []
-                            ) Positive
-                            ( Relation
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 27
-                                    , locColumn = 33
-                                    }
-                                )
-                                ( RelationSymbol
-                                    ( Command "in" )
-                                    ( ParameterArity 0 )
-                                    ( Marker "elem" )
-                                ) []
-                            )
-                            ( ExprOp
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 27
-                                    , locColumn = 36
-                                    }
-                                )
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "fin" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "fin" ) NonAssoc
-                                )
-                                [ ExprVar
-                                    ( NamedVar "A" )
-                                ] :| []
-                            )
-                        )
-                    ]
-                , introResult = FormulaChain
-                    ( ChainBase
-                        ( ExprOp
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 52
-                                }
-                            )
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "cons" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons
-                                            ( TokenCons InvisibleBraceR
-                                                ( TokenCons InvisibleBraceL
-                                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                                )
-                                            )
-                                        )
-                                    )
-                                )
-                                ( Marker "cons" ) NonAssoc
-                            )
-                            [ ExprVar
-                                ( NamedVar "a" )
-                            , ExprVar
-                                ( NamedVar "B" )
-                            ] :| []
-                        ) Positive
-                        ( Relation
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 63
-                                }
-                            )
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            ) []
-                        )
-                        ( ExprOp
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 27
-                                , locColumn = 66
-                                }
-                            )
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "fin" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "fin" ) NonAssoc
-                            )
-                            [ ExprVar
-                                ( NamedVar "A" )
-                            ] :| []
-                        )
-                    )
-                }
-            ]
-        }
-    )
-, BlockClaim Proposition
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 31
-        , locColumn = 1
-        }
-    ) Nothing
-    ( Marker "fin_intro_ref" )
-    ( Claim []
-        ( StmtFormula
-            { formula = FormulaChain
-                ( ChainBase
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 32
-                            , locColumn = 6
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "emptyset" ) End
-                            )
-                            ( Marker "emptyset" ) NonAssoc
-                        ) [] :| []
+                    ( ExprVar
+                        ( NamedVar "A" ) :| []
                     ) Positive
                     ( Relation
                         ( Location
                             { locFile = "test/examples/inductive.tex"
-                            , locLine = 32
-                            , locColumn = 16
+                            , locLine = 6
+                            , locColumn = 17
                             }
                         )
                         ( RelationSymbol
@@ -480,7 +60,7 @@
                     ( ExprOp
                         ( Location
                             { locFile = "test/examples/inductive.tex"
-                            , locLine = 32
+                            , locLine = 6
                             , locColumn = 20
                             }
                         )
@@ -498,172 +78,6 @@
                         ] :| []
                     )
                 )
-            }
-        )
-    )
-, BlockProof
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 34
-        , locColumn = 1
-        }
-    )
-    ( Qed
-        ( Just
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 35
-                , locColumn = 5
-                }
-            )
-        )
-        ( JustificationRef
-            ( Marker "fin_intro_1" :| [] )
-        )
-    )
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 36
-        , locColumn = 1
-        }
-    )
-, BlockInductive
-    ( Location
-        { locFile = "test/examples/inductive.tex"
-        , locLine = 38
-        , locColumn = 1
-        }
-    ) Nothing
-    ( Marker "acc" )
-    ( Inductive
-        { inductiveSymbolPattern = SymbolPattern
-            ( MixfixItem
-                ( TokenCons
-                    ( Command "acc" )
-                    ( TokenCons InvisibleBraceL
-                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                    )
-                )
-                ( Marker "acc" ) NonAssoc
-            )
-            [ NamedVar "R" ]
-        , inductiveDomain = ExprOp
-            ( Location
-                { locFile = "test/examples/inductive.tex"
-                , locLine = 39
-                , locColumn = 29
-                }
-            )
-            ( MixfixItem
-                ( TokenCons
-                    ( Command "wrap" )
-                    ( TokenCons InvisibleBraceL
-                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                    )
-                )
-                ( Marker "wrap" ) NonAssoc
-            )
-            [ ExprVar
-                ( NamedVar "R" )
-            ]
-        , inductiveIntros = IntroRule
-            { introConditions =
-                [ FormulaChain
-                    ( ChainBase
-                        ( ExprVar
-                            ( NamedVar "x" ) :| []
-                        ) Positive
-                        ( Relation
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 41
-                                , locColumn = 20
-                                }
-                            )
-                            ( RelationSymbol
-                                ( Command "in" )
-                                ( ParameterArity 0 )
-                                ( Marker "elem" )
-                            ) []
-                        )
-                        ( ExprOp
-                            ( Location
-                                { locFile = "test/examples/inductive.tex"
-                                , locLine = 41
-                                , locColumn = 23
-                                }
-                            )
-                            ( MixfixItem
-                                ( TokenCons
-                                    ( Command "wrap" )
-                                    ( TokenCons InvisibleBraceL
-                                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                    )
-                                )
-                                ( Marker "wrap" ) NonAssoc
-                            )
-                            [ ExprOp
-                                ( Location
-                                    { locFile = "test/examples/inductive.tex"
-                                    , locLine = 41
-                                    , locColumn = 29
-                                    }
-                                )
-                                ( MixfixItem
-                                    ( TokenCons
-                                        ( Command "acc" )
-                                        ( TokenCons InvisibleBraceL
-                                            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                        )
-                                    )
-                                    ( Marker "acc" ) NonAssoc
-                                )
-                                [ ExprVar
-                                    ( NamedVar "R" )
-                                ]
-                            ] :| []
-                        )
-                    )
-                ]
-            , introResult = FormulaChain
-                ( ChainBase
-                    ( ExprVar
-                        ( NamedVar "x" ) :| []
-                    ) Positive
-                    ( Relation
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 41
-                            , locColumn = 47
-                            }
-                        )
-                        ( RelationSymbol
-                            ( Command "in" )
-                            ( ParameterArity 0 )
-                            ( Marker "elem" )
-                        ) []
-                    )
-                    ( ExprOp
-                        ( Location
-                            { locFile = "test/examples/inductive.tex"
-                            , locLine = 41
-                            , locColumn = 50
-                            }
-                        )
-                        ( MixfixItem
-                            ( TokenCons
-                                ( Command "acc" )
-                                ( TokenCons InvisibleBraceL
-                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
-                                )
-                            )
-                            ( Marker "acc" ) NonAssoc
-                        )
-                        [ ExprVar
-                            ( NamedVar "R" )
-                        ] :| []
-                    )
-                )
             } :| []
         }
     )
diff --git a/test/golden/inductive/scanning.golden b/test/golden/inductive/scanning.golden
index 28c82d8..3807c98 100644
--- a/test/golden/inductive/scanning.golden
+++ b/test/golden/inductive/scanning.golden
@@ -1,25 +1,9 @@
 [ ScanFunctionSymbol
     ( TokenCons
-        ( Command "wrap" )
-        ( TokenCons InvisibleBraceL
-            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-        )
-    )
-    ( Marker "wrap" )
-, ScanFunctionSymbol
-    ( TokenCons
         ( Command "fin" )
         ( TokenCons InvisibleBraceL
             ( HoleCons ( TokenCons InvisibleBraceR End ) )
         )
     )
     ( Marker "fin" )
-, ScanFunctionSymbol
-    ( TokenCons
-        ( Command "acc" )
-        ( TokenCons InvisibleBraceL
-            ( HoleCons ( TokenCons InvisibleBraceR End ) )
-        )
-    )
-    ( Marker "acc" )
 ]
\ No newline at end of file
diff --git a/test/golden/inductive/tokenizing.golden b/test/golden/inductive/tokenizing.golden
index 28527ec..f432041 100644
--- a/test/golden/inductive/tokenizing.golden
+++ b/test/golden/inductive/tokenizing.golden
@@ -1,60 +1,4 @@
 [
-    [ BeginEnv "axiom"
-    , Label "pow"
-    , BeginEnv "math"
-    , Command "pow"
-    , InvisibleBraceL
-    , Variable "A"
-    , InvisibleBraceR
-    , Symbol "="
-    , Command "emptyset"
-    , EndEnv "math"
-    , Symbol "."
-    , EndEnv "axiom"
-    ]
-,
-    [ BeginEnv "axiom"
-    , Label "cons"
-    , BeginEnv "math"
-    , Command "cons"
-    , InvisibleBraceL
-    , Variable "a"
-    , InvisibleBraceR
-    , InvisibleBraceL
-    , Variable "B"
-    , InvisibleBraceR
-    , Symbol "="
-    , Command "emptyset"
-    , EndEnv "math"
-    , Symbol "."
-    , EndEnv "axiom"
-    ]
-,
-    [ BeginEnv "definition"
-    , Label "wrap"
-    , BeginEnv "math"
-    , Command "wrap"
-    , InvisibleBraceL
-    , Variable "A"
-    , InvisibleBraceR
-    , Symbol "="
-    , Command "emptyset"
-    , EndEnv "math"
-    , Symbol "."
-    , EndEnv "definition"
-    ]
-,
-    [ BeginEnv "axiom"
-    , Label "everything_in_emptyset"
-    , BeginEnv "math"
-    , Variable "x"
-    , Command "in"
-    , Command "emptyset"
-    , EndEnv "math"
-    , Symbol "."
-    , EndEnv "axiom"
-    ]
-,
     [ BeginEnv "inductive"
     , Label "fin"
     , Word "define"
@@ -64,7 +8,7 @@
     , Variable "A"
     , InvisibleBraceR
     , Command "subseteq"
-    , Command "pow"
+    , Command "cumul"
     , InvisibleBraceL
     , Variable "A"
     , InvisibleBraceR
@@ -76,116 +20,13 @@
     , BeginEnv "enumerate"
     , Command "item"
     , BeginEnv "math"
-    , Command "emptyset"
-    , Command "in"
-    , Command "fin"
-    , InvisibleBraceL
     , Variable "A"
-    , InvisibleBraceR
-    , EndEnv "math"
-    , Symbol "."
-    , Command "item"
-    , Word "if"
-    , BeginEnv "math"
-    , Variable "a"
-    , Command "in"
-    , Variable "A"
-    , EndEnv "math"
-    , Word "and"
-    , BeginEnv "math"
-    , Variable "B"
     , Command "in"
     , Command "fin"
     , InvisibleBraceL
     , Variable "A"
     , InvisibleBraceR
     , EndEnv "math"
-    , Symbol ","
-    , Word "then"
-    , BeginEnv "math"
-    , Command "cons"
-    , InvisibleBraceL
-    , Variable "a"
-    , InvisibleBraceR
-    , InvisibleBraceL
-    , Variable "B"
-    , InvisibleBraceR
-    , Command "in"
-    , Command "fin"
-    , InvisibleBraceL
-    , Variable "A"
-    , InvisibleBraceR
-    , EndEnv "math"
-    , Symbol "."
-    , EndEnv "enumerate"
-    , EndEnv "inductive"
-    ]
-,
-    [ BeginEnv "proposition"
-    , Label "fin_intro_ref"
-    , BeginEnv "math"
-    , Command "emptyset"
-    , Command "in"
-    , Command "fin"
-    , InvisibleBraceL
-    , Variable "A"
-    , InvisibleBraceR
-    , EndEnv "math"
-    , Symbol "."
-    , EndEnv "proposition"
-    ]
-,
-    [ BeginEnv "proof"
-    , Word "follows"
-    , Word "by"
-    , Ref
-        ( "fin_intro_1" :| [] )
-    , Symbol "."
-    , EndEnv "proof"
-    ]
-,
-    [ BeginEnv "inductive"
-    , Label "acc"
-    , Word "define"
-    , BeginEnv "math"
-    , Command "acc"
-    , InvisibleBraceL
-    , Variable "R"
-    , InvisibleBraceR
-    , Command "subseteq"
-    , Command "wrap"
-    , InvisibleBraceL
-    , Variable "R"
-    , InvisibleBraceR
-    , EndEnv "math"
-    , Word "inductively"
-    , Word "as"
-    , Word "follows"
-    , Symbol "."
-    , BeginEnv "enumerate"
-    , Command "item"
-    , Word "if"
-    , BeginEnv "math"
-    , Variable "x"
-    , Command "in"
-    , Command "wrap"
-    , InvisibleBraceL
-    , Command "acc"
-    , InvisibleBraceL
-    , Variable "R"
-    , InvisibleBraceR
-    , InvisibleBraceR
-    , EndEnv "math"
-    , Symbol ","
-    , Word "then"
-    , BeginEnv "math"
-    , Variable "x"
-    , Command "in"
-    , Command "acc"
-    , InvisibleBraceL
-    , Variable "R"
-    , InvisibleBraceR
-    , EndEnv "math"
     , Symbol "."
     , EndEnv "enumerate"
     , EndEnv "inductive"
diff --git a/test/golden/inductive/verification.golden b/test/golden/inductive/verification.golden
index 3396b0d..f4c7d7a 100644
--- a/test/golden/inductive/verification.golden
+++ b/test/golden/inductive/verification.golden
@@ -1,10 +1,10 @@
 VerifiedWithTrustedVampire
     ( VerificationReport
-        { verificationLegacyDeclaredAssumptionCount = 3
+        { verificationLegacyDeclaredAssumptionCount = 0
         , verificationTypedDeclaredAssumptionCount = 0
-        , verificationTrustedVampireCount = 5
+        , verificationTrustedVampireCount = 0
         , verificationExplicitGapLocations = []
-        , verificationTrustedLegacyRuleCount = 10
-        , verificationKernelProofCount = 0
+        , verificationTrustedLegacyRuleCount = 0
+        , verificationKernelProofCount = 4
         }
     )
\ No newline at end of file