Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 2639 deletions

diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs
deleted file mode 100644
index 92ff500..0000000
--- a/source/Checking/Exact/Proof.hs
+++ /dev/null
@@ -1,2639 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Exact lowering for the first ordinary theorem/proof fragment.
---
--- This module is the trusted owner of structural local-proof composition.  Its
--- private prepared tree controls when assumptions and proved local claims
--- become available and executes discharges depth-first.  The declaration
--- boundary validates typed tasks and authority; it does not reconstruct this
--- derivation.
-module Checking.Exact.Proof
-    ( PreparedExactProof
-    , preparedExactProofSyntaxId
-    , preparedExactProofFirstOmission
-    , prepareExactProof
-    , CheckedExactProofAuthorization
-    , lowerPreparedExactProof
-    , authorizeCheckedExactProof
-    , PreparedFinalPreludeFoundationClaim
-    , prepareFinalPreludeFoundationClaim
-    , CheckedFinalPreludeFoundationAuthorization
-    , lowerPreparedFinalPreludeFoundationClaim
-    , authorizeCheckedFinalPreludeFoundationClaim
-    , ExactProofError(..)
-    , exactProofErrorLocation
-    , renderExactProofError
-    ) where
-
-import Base
-import Checking.Authority qualified as Authority
-import Checking.Backend.Problem qualified as Backend
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact qualified as Exact
-import Checking.Foundation
-import Checking.Identity
-import Checking.Kernel.Derivation (foundationFactDerivation)
-import Checking.Kernel.Proof qualified as KernelProof
-import Checking.SetConstruction
-import Checking.Semantic
-import Felix.Cache.Codec
-import Report.Location
-import Syntax.Abstract qualified as Raw
-
-import Control.Monad.Except (ExceptT)
-import Control.Monad.Except qualified as Except
-import Control.Monad (foldM, unless, when)
-import Control.Monad.State.Strict (StateT)
-import Control.Monad.State.Strict qualified as State
-import Data.ByteString (ByteString)
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Data.Vector (Vector)
-import Data.Vector qualified as Vector
-import Numeric.Natural (Natural)
-
-
-data ExactProofError
-    = ExactProofUnsupportedClaim !Location
-    | ExactProofUnsupportedStep !Location
-    | ExactProofSetInductionVariableRequired !Location
-    | ExactProofSetInductionVariableNotActive
-        !Location !Raw.VarSymbol
-    | ExactProofSetInductionFocusAmbiguous !Location
-    | ExactProofSetInductionActiveBinderIneligible
-        !Location !Raw.VarSymbol
-    | ExactProofSetInductionBinderConflict
-        !Location !Raw.VarSymbol
-    | ExactProofSetInductionGoalMismatch !Location
-    | ExactProofSetExtensionalityGoalMismatch !Location
-    | ExactProofSetExtensionalityDirectionsUnavailable !Location
-    | ExactProofExpectedUniversalGoal !Location
-    | ExactProofExpectedImplicationGoal !Location
-    | ExactProofGoalStatementMismatch !Location
-    | ExactProofEmptyCaseSplit !Location
-    | ExactProofStructuralCompositionFailed
-        !Location !KernelProof.KernelProofBuildError
-    | ExactProofLocalFunctionBinderMismatch !Location
-    | ExactProofLocalFunctionNameConflict !Location
-    | ExactProofUnknownReference !Location !Raw.Marker
-    | ExactProofElaborationFailed !Exact.ExactCompileError
-    | ExactProofObligationPreparationFailed
-        !Location
-        !(Declaration.VampireObligationPreparationError
-            Exact.ExactLocalId)
-    | ExactProofFoundationLeafRequiresImplicitAuto !Location
-    | ExactProofFoundationLeafTargetMismatch !Location
-    | ExactProofFoundationLeafTargetAmbiguous !Location
-    deriving stock (Show, Eq)
-
-exactProofErrorLocation :: ExactProofError -> Location
-exactProofErrorLocation = \case
-    ExactProofUnsupportedClaim location -> location
-    ExactProofUnsupportedStep location -> location
-    ExactProofSetInductionVariableRequired location -> location
-    ExactProofSetInductionVariableNotActive location _variable ->
-        location
-    ExactProofSetInductionFocusAmbiguous location -> location
-    ExactProofSetInductionActiveBinderIneligible location _variable ->
-        location
-    ExactProofSetInductionBinderConflict location _variable ->
-        location
-    ExactProofSetInductionGoalMismatch location -> location
-    ExactProofSetExtensionalityGoalMismatch location -> location
-    ExactProofSetExtensionalityDirectionsUnavailable location -> location
-    ExactProofExpectedUniversalGoal location -> location
-    ExactProofExpectedImplicationGoal location -> location
-    ExactProofGoalStatementMismatch location -> location
-    ExactProofEmptyCaseSplit location -> location
-    ExactProofStructuralCompositionFailed location _failure -> location
-    ExactProofLocalFunctionBinderMismatch location -> location
-    ExactProofLocalFunctionNameConflict location -> location
-    ExactProofUnknownReference location _marker -> location
-    ExactProofElaborationFailed failure ->
-        Exact.exactCompileErrorLocation failure
-    ExactProofObligationPreparationFailed location _failure -> location
-    ExactProofFoundationLeafRequiresImplicitAuto location -> location
-    ExactProofFoundationLeafTargetMismatch location -> location
-    ExactProofFoundationLeafTargetAmbiguous location -> location
-
-renderExactProofError :: ExactProofError -> Text
-renderExactProofError = \case
-    ExactProofUnsupportedClaim location ->
-        at location <> "this claim is not yet supported by the typed checker"
-    ExactProofUnsupportedStep location ->
-        at location <> "this proof step is not yet supported by the typed checker"
-    ExactProofSetInductionVariableRequired location ->
-        at location <> "exact set induction requires a named set variable"
-    ExactProofSetInductionVariableNotActive location variable ->
-        at location <> "the set-induction variable " <> shown variable
-            <> " is not an eligible exact focus"
-    ExactProofSetInductionFocusAmbiguous location ->
-        at location
-            <> "set induction without an explicit variable has no unique focus"
-    ExactProofSetInductionActiveBinderIneligible location variable ->
-        at location <> "the active binder " <> shown variable
-            <> " is not an eligible set-induction focus"
-    ExactProofSetInductionBinderConflict location variable ->
-        at location <> "the leading set-induction binder " <> shown variable
-            <> " conflicts with an active exact binder"
-    ExactProofSetInductionGoalMismatch location ->
-        at location <> "the set-induction variable does not belong to this goal"
-    ExactProofSetExtensionalityGoalMismatch location ->
-        at location <> "set extensionality requires a set-equality goal"
-    ExactProofSetExtensionalityDirectionsUnavailable location ->
-        at location
-            <> "set extensionality requires both directions as proved local claims"
-    ExactProofExpectedUniversalGoal location ->
-        at location <> "this fix step requires a universal goal"
-    ExactProofExpectedImplicationGoal location ->
-        at location <> "this assume step requires an implication goal"
-    ExactProofGoalStatementMismatch location ->
-        at location <> "the proof step does not match the current goal"
-    ExactProofEmptyCaseSplit location ->
-        at location <> "case analysis requires at least one case"
-    ExactProofStructuralCompositionFailed location failure ->
-        at location <> "invalid structural proof composition: " <> shown failure
-    ExactProofLocalFunctionBinderMismatch location ->
-        at location <> "the function argument must match its domain binder"
-    ExactProofLocalFunctionNameConflict location ->
-        at location <> "the function and argument names must be distinct"
-    ExactProofUnknownReference location marker ->
-        at location <> "the cited fact " <> shown marker <> " is not visible"
-    ExactProofElaborationFailed failure ->
-        Exact.renderExactCompileError failure
-    ExactProofObligationPreparationFailed location failure ->
-        at location <> "the exact proof obligation is invalid: " <> shown failure
-    ExactProofFoundationLeafRequiresImplicitAuto location ->
-        at location
-            <> "a confined foundation claim requires an implicit Auto proof"
-    ExactProofFoundationLeafTargetMismatch location ->
-        at location <> "the claim does not exactly match a foundation axiom"
-    ExactProofFoundationLeafTargetAmbiguous location ->
-        at location <> "the claim matches more than one foundation axiom"
-  where
-    at location = locationToText location <> ": "
-    shown :: Show value => value -> Text
-    shown = Text.pack . show
-
-data ExactLocalOrigin
-    = ExactAssumption
-    | ExactDerivedClaim
-    | ExactLocalDefinition
-    | ExactLocalConstructionExtensional
-    | ExactLocalConstructionEquation
-    deriving stock (Show, Eq, Ord)
-
-data PreparedLocal = PreparedLocal
-    !Backend.LocalPremiseOrdinal
-    !ExactLocalOrigin
-    !(Vector (Exact.ExactLocalId, CoreType))
-    !(ScopedCheckedCore ObjectId)
-
-data PreparedJustification
-    = PreparedAuto
-    | PreparedReferences
-        !(NonEmpty SemanticFactOccurrenceFingerprint)
-    | PreparedLocalOnly
-
-data PreparedDischarge
-    = PreparedVampireDischarge
-        !Location
-        !PreparedJustification
-        !(ScopedCheckedCore ObjectId)
-        !(Declaration.PreparedVampireObligation
-            Exact.ExactLocalId
-            ExactLocalOrigin)
-    | PreparedSetExtensionality
-        !Location
-        !(ScopedCheckedCore ObjectId)
-
-data PreparedCalculationLink = PreparedCalculationLink
-    !(ScopedCheckedCore ObjectId)
-    !PreparedDischarge
-
--- The private constructor stores every destination with the discharge derived
--- from its immediately preceding endpoint.  Planning and admission can
--- therefore traverse one immutable sequence without re-associating shapes.
-data PreparedCalculation = PreparedCheckedCalculation
-    !CoreType
-    ![Exact.ExactLocalId]
-    !(Maybe (ScopedCheckedCore ObjectId))
-    !(ScopedCheckedCore ObjectId)
-    !(NonEmpty PreparedCalculationLink)
-    !(ScopedCheckedCore ObjectId)
-
-data PreparedSinceEvidence
-    = PreparedSinceExisting !PreparedLocal
-    | PreparedSinceDischarged !PreparedDischarge !PreparedLocal
-
-data PreparedCase = PreparedCase
-    !(ScopedCheckedCore ObjectId)
-    !PreparedProof
-
-data PreparedCaseAnalysis = PreparedCaseAnalysis
-    !(ScopedCheckedCore ObjectId)
-    !(NonEmpty PreparedCase)
-    !(ScopedCheckedCore ObjectId)
-    !PreparedDischarge
-
-data InitialSetInductionFocus = InitialSetInductionFocus
-    !Raw.VarSymbol
-    !Exact.ExactLocalId
-    !Natural
-
-data InitialSetInductionView = InitialSetInductionView
-    ![InitialSetInductionFocus]
-    !(Vector (Exact.ExactLocalId, CoreType))
-    !(ScopedCheckedCore ObjectId)
-    ![ScopedCheckedCore ObjectId]
-    !(ScopedCheckedCore ObjectId)
-    !(Maybe Raw.VarSymbol)
-
-data SetInductionBoundary
-    = InitialClaimInduction !InitialSetInductionView
-    -- A direct source-statement goal may retain only its leading binder name.
-    -- Recursive proof transformations deliberately discard this hint.
-    | SourceStatementInduction !(Maybe Raw.VarSymbol)
-    | RecursiveProofInduction
-
-data SelectedSetInductionFocus
-    = SelectedInitialSetInduction !InitialSetInductionFocus
-    | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol)
-
-data PreparedSetInductionFocus
-    = PreparedInitialSetInductionFocus
-        !Exact.ExactLocalId
-        !Natural
-    | PreparedLeadingSetInductionFocus
-        !Exact.ExactLocalId
-
-data PreparedSetInduction = PreparedCheckedSetInduction
-    !PreparedSetInductionFocus
-    !(ScopedCheckedCore ObjectId)
-    ![ScopedCheckedCore ObjectId]
-    !(ScopedCheckedCore ObjectId)
-    !(ScopedCheckedCore ObjectId)
-    !(ScopedCheckedCore ObjectId)
-    !PreparedProof
-
-data PreparedProof
-    = PreparedImplicitAuto !PreparedDischarge
-    | PreparedQed !PreparedDischarge
-    | PreparedOmitted
-        !Location
-        !(ScopedCheckedCore ObjectId)
-    | PreparedFix ![Exact.ExactLocalId] !PreparedProof
-    | PreparedAssume
-        !(ScopedCheckedCore ObjectId)
-        !PreparedProof
-    | PreparedTake
-        ![Exact.ExactLocalId]
-        !(ScopedCheckedCore ObjectId)
-        !PreparedDischarge
-        !PreparedProof
-    | PreparedSetInduction !PreparedSetInduction
-    | PreparedHave
-        !(ScopedCheckedCore ObjectId)
-        !PreparedDischarge
-        !PreparedProof
-    | PreparedSuffices
-        !(ScopedCheckedCore ObjectId)
-        !(ScopedCheckedCore ObjectId)
-        !(ScopedCheckedCore ObjectId)
-        !PreparedDischarge
-        !PreparedProof
-    | PreparedCalculate
-        !PreparedCalculation
-        !PreparedProof
-    | PreparedSince
-        !(ScopedCheckedCore ObjectId)
-        !PreparedSinceEvidence
-        !(ScopedCheckedCore ObjectId)
-        !PreparedDischarge
-        !PreparedProof
-    | PreparedSubclaim
-        !(ScopedCheckedCore ObjectId)
-        !PreparedProof
-        !PreparedProof
-    | PreparedDefine
-        !Exact.ExactLocalId
-        !(ScopedCheckedCore ObjectId)
-        !(NonEmpty (ScopedCheckedCore ObjectId))
-        !PreparedProof
-    | PreparedDefineRelational
-        !Exact.ExactLocalId
-        !(ScopedCheckedCore ObjectId)
-        !PreparedDischarge
-        !(NonEmpty (ScopedCheckedCore ObjectId))
-        !PreparedProof
-    | PreparedDefineFunction
-        !Exact.ExactLocalId
-        !(ScopedCheckedCore ObjectId)
-        !(ScopedCheckedCore ObjectId)
-        !PreparedProof
-    | PreparedByCase !PreparedCaseAnalysis
-    | PreparedByContradiction
-        !(ScopedCheckedCore ObjectId)
-        !(ScopedCheckedCore ObjectId)
-        !(ScopedCheckedCore ObjectId)
-        !PreparedProof
-    | PreparedContradiction
-        !(ScopedCheckedCore ObjectId)
-        !(ScopedCheckedCore ObjectId)
-        !PreparedDischarge
-
-data PreparedExactProof = PreparedExactProof
-    !Location
-    !SemanticName
-    !(ScopedCheckedCore ObjectId)
-    !PreparedProof
-    !ProofSyntaxId
-
-data PreparedFinalPreludeFoundationClaim =
-    PreparedFinalPreludeFoundationClaim
-    !Location
-    !SemanticName
-    !(ScopedCheckedCore ObjectId)
-    !FoundationAxiomTag
-    !ProofSyntaxId
-
-preparedExactProofSyntaxId :: PreparedExactProof -> ProofSyntaxId
-preparedExactProofSyntaxId
-        (PreparedExactProof _location _alias _target _proof syntax) =
-    syntax
-
-preparedExactProofFirstOmission :: PreparedExactProof -> Maybe Location
-preparedExactProofFirstOmission
-        (PreparedExactProof _location _alias _target proof _syntax) =
-    preparedProofFirstOmission proof
-
-data PrepareState = PrepareState
-    { prepareNextLocal :: !Natural
-    , prepareNextPremise :: !Natural
-    }
-
-type Prepare =
-    StateT
-        PrepareState
-        (ExceptT ExactProofError (Declaration.LoweringDriver))
-
-prepareExactProof
-    :: Raw.Block
-    -> Maybe Raw.Proof
-    -> Declaration.LoweringDriver
-        (Either ExactProofError PreparedExactProof)
-prepareExactProof block explicitProof =
-    Except.runExceptT
-        (State.evalStateT prepare initialState)
-  where
-    initialState = PrepareState 0 0
-
-    prepare =
-        case block of
-            Raw.BlockClaim
-                    _kind location _title (Raw.Marker marker)
-                    (Raw.Claim assumptions statement) -> do
-                envelope <-
-                    liftDriver
-                        (Exact.prepareExactClaimEnvelope assumptions statement)
-                        >>= either
-                            (throwProof . ExactProofElaborationFailed)
-                            pure
-                let targetCore = Exact.preparedExactClaimTarget envelope
-                unless (null (scopedCoreContext targetCore))
-                    (throwProof
-                        (ExactProofUnsupportedClaim location))
-                (context, openedGoal, identities) <-
-                    openEnvelopeVariables
-                        targetCore
-                        (Exact.preparedExactClaimVariables envelope)
-                        (Exact.preparedExactClaimContext envelope)
-                (locals, bodyGoal, antecedents) <-
-                    openEnvelopeAntecedents
-                        context
-                        openedGoal
-                        (Exact.preparedExactClaimAntecedentCount envelope)
-                initialInduction <-
-                    prepareInitialSetInductionView
-                        statement
-                        context
-                        (Exact.preparedExactClaimVariables envelope)
-                        identities
-                        antecedents
-                        bodyGoal
-                bodyProof <-
-                    case explicitProof of
-                        Nothing ->
-                            PreparedImplicitAuto
-                                <$> prepareDischarge
-                                    location
-                                    context
-                                    locals
-                                    bodyGoal
-                                    Raw.JustificationEmpty
-                        Just sourceProof ->
-                            prepareProof
-                                location
-                                context
-                                locals
-                                (InitialClaimInduction initialInduction)
-                                bodyGoal
-                                sourceProof
-                let withAssumptions =
-                        foldr PreparedAssume bodyProof antecedents
-                    proof =
-                        case identities of
-                            [] -> withAssumptions
-                            _ -> PreparedFix identities withAssumptions
-                pure
-                    (PreparedExactProof
-                        location
-                        (semanticName marker)
-                        targetCore
-                        proof
-                        (proofSyntaxId
-                            (encodePreparedProof proof)))
-            _ ->
-                throwProof
-                    (ExactProofUnsupportedClaim (locate block))
-
-prepareFinalPreludeFoundationClaim
-    :: CheckedFoundation
-    -> Raw.Block
-    -> Maybe Raw.Proof
-    -> Declaration.LoweringDriver
-        (Either ExactProofError PreparedFinalPreludeFoundationClaim)
-prepareFinalPreludeFoundationClaim foundation block explicitProof =
-    Except.runExceptT do
-        case (block, explicitProof) of
-            ( Raw.BlockClaim
-                    _kind location _title (Raw.Marker marker)
-                    (Raw.Claim assumptions statement)
-              , Nothing
-              ) -> do
-                envelope <-
-                    Except.lift
-                        (Exact.prepareExactClaimEnvelope
-                            assumptions
-                            statement)
-                        >>= either
-                            (Except.throwError
-                                . ExactProofElaborationFailed)
-                            pure
-                unless
-                    ( null (Exact.preparedExactClaimVariables envelope)
-                        && Exact.preparedExactClaimAntecedentCount envelope
-                            == 0
-                    )
-                    (Except.throwError
-                        (ExactProofFoundationLeafRequiresImplicitAuto
-                            location))
-                let target = Exact.preparedExactClaimTarget envelope
-                    matches =
-                        [ tag
-                        | tag <- [minBound .. maxBound]
-                        , target == foundationTarget tag
-                        ]
-                tag <- case matches of
-                    [] ->
-                        Except.throwError
-                            (ExactProofFoundationLeafTargetMismatch location)
-                    [only] ->
-                        pure only
-                    _ ->
-                        Except.throwError
-                            (ExactProofFoundationLeafTargetAmbiguous location)
-                pure
-                    (PreparedFinalPreludeFoundationClaim
-                        location
-                        (semanticName marker)
-                        target
-                        tag
-                        (implicitAutoProofSyntaxId target))
-            (Raw.BlockClaim _kind location _title _marker _claim, Just{}) ->
-                Except.throwError
-                    (ExactProofFoundationLeafRequiresImplicitAuto location)
-            _ ->
-                Except.throwError
-                    (ExactProofUnsupportedClaim (locate block))
-  where
-    foundationTarget tag =
-        embedClosedCore []
-            (mapFrozenGlobals
-                absurd
-                (foundationAxiomFrozen foundation tag))
-
-openEnvelopeVariables
-    :: ScopedCheckedCore ObjectId
-    -> [Raw.VarSymbol]
-    -> Exact.ExactBinderContext
-    -> Prepare
-        ( Exact.ExactBinderContext
-        , ScopedCheckedCore ObjectId
-        , [Exact.ExactLocalId]
-        )
-openEnvelopeVariables target variables preparedContext =
-    case NonEmpty.nonEmpty variables of
-        Nothing ->
-            pure (preparedContext, target, [])
-        Just nonempty -> do
-            (_unannotated, opened, identities) <-
-                openFixedVariables
-                Exact.emptyExactBinderContext
-                target
-                nonempty
-            let expected =
-                    reverse
-                        (fst <$> toList
-                            (Exact.exactBinderContextSupport preparedContext))
-            unless
-                (identities == expected)
-                (impossible
-                    "prepared claim annotations do not match opened binders")
-            pure (preparedContext, opened, identities)
-
-openEnvelopeAntecedents
-    :: Exact.ExactBinderContext
-    -> ScopedCheckedCore ObjectId
-    -> Natural
-    -> Prepare
-        ( [PreparedLocal]
-        , ScopedCheckedCore ObjectId
-        , [ScopedCheckedCore ObjectId]
-        )
-openEnvelopeAntecedents context initialGoal initialCount =
-    go [] [] initialGoal initialCount
-  where
-    go locals antecedents goal 0 =
-        pure (locals, goal, antecedents)
-    go locals antecedents goal remaining = do
-        (antecedent, conclusion) <-
-            maybe
-                (impossible
-                    "a prepared claim envelope has too few implications")
-                pure
-                (openScopedImplication goal)
-        local <- allocateLocal ExactAssumption context antecedent
-        go
-            (locals <> [local])
-            (antecedents <> [antecedent])
-            conclusion
-            (remaining - 1)
-
-prepareInitialSetInductionView
-    :: Raw.Stmt
-    -> Exact.ExactBinderContext
-    -> [Raw.VarSymbol]
-    -> [Exact.ExactLocalId]
-    -> [ScopedCheckedCore ObjectId]
-    -> ScopedCheckedCore ObjectId
-    -> Prepare InitialSetInductionView
-prepareInitialSetInductionView
-        statement context variables identities antecedents bodyGoal = do
-    unless (length variables == length identities)
-        (impossible
-            "opened claim binders lost their source identity association")
-    foci <- traverse checkedFocus (zip variables identities)
-    let property = foldr implyChecked bodyGoal antecedents
-        support = Exact.exactBinderContextSupport context
-    unless
-        ( scopedCoreContext property
-            == (snd <$> Vector.toList support)
-        )
-        (impossible
-            "initial set-induction property changed its checked context")
-    pure
-        (InitialSetInductionView
-            foci support property antecedents bodyGoal
-            (claimLeadingUniversalName statement))
-  where
-    checkedFocus (variable, identity) = do
-        index <-
-            maybe
-                (impossible
-                    "an opened claim binder is absent from its exact context")
-                pure
-                (Exact.exactBinderContextIndex variable context)
-        case Exact.exactBinderContextSupport context
-                Vector.!? (fromIntegral index) of
-            Just (actualIdentity, TySet)
-                | actualIdentity == identity ->
-                    pure
-                        (InitialSetInductionFocus
-                            variable identity index)
-            _ ->
-                impossible
-                    "an initial set-induction focus changed identity or type"
-
-    implyChecked antecedent conclusion =
-        fromMaybe
-            (impossible
-                "an exact claim antecedent changed context")
-            (implyScopedCore antecedent conclusion)
-
-claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol
-claimLeadingUniversalName = \case
-    Raw.StmtFormula
-            (Raw.FormulaQuantified _location Raw.Universally
-                (variable :| _rest) _bound _formula) ->
-        Just variable
-    Raw.SymbolicForall _location (variable :| _rest)
-            _bound _suchThat _statement ->
-        Just variable
-    Raw.StmtQuantPhrase
-            _location
-            (Raw.QuantPhrase Raw.Universally
-                (Raw.NounPhrase _left _noun variables _right _suchThat))
-            _statement ->
-        listToMaybe variables
-    Raw.StmtVerbPhrase
-            (Raw.TermQuantified Raw.Universally _location
-                (Raw.NounPhrase _left _noun variable _right _suchThat)
-                :| [])
-            _verb ->
-        variable
-    Raw.StmtNoun
-            (Raw.TermQuantified Raw.Universally _location
-                (Raw.NounPhrase _left _noun variable _right _suchThat)
-                :| [])
-            _nounPhrase ->
-        variable
-    _statement ->
-        Nothing
-
-prepareProof
-    :: Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> SetInductionBoundary
-    -> ScopedCheckedCore ObjectId
-    -> Raw.Proof
-    -> Prepare PreparedProof
-prepareProof fallback context locals inductionBoundary goal = \case
-    Raw.Omitted location ->
-        pure (PreparedOmitted location goal)
-    Raw.Qed maybeLocation justification ->
-        PreparedQed
-            <$> prepareDischarge
-                (fromMaybe fallback maybeLocation)
-                context
-                locals
-                goal
-                justification
-    Raw.FixSymbolic location variables bound continuation -> do
-        (context', goal', identities) <-
-            openFixedVariables context goal variables
-        case bound of
-            Raw.Unbounded ->
-                PreparedFix identities
-                    <$> prepareProof
-                        fallback
-                        context'
-                        locals
-                        RecursiveProofInduction
-                        goal'
-                        continuation
-            _ -> do
-                constraint <-
-                    prepareSymbolicBoundConstraints
-                        context' variables bound
-                prepareGuardedFix
-                    fallback location context' locals goal'
-                    identities constraint continuation
-    Raw.FixSuchThat location variables statement continuation -> do
-        (context', goal', identities) <-
-            openFixedVariables context goal variables
-        constraint <-
-            Exact.preparedExactPropositionCore
-                <$> prepareStatement context' statement
-        prepareGuardedFix
-            fallback location context' locals goal'
-            identities constraint continuation
-    Raw.Assume location statement continuation -> do
-        supplied <- prepareStatement context statement
-        when (isNothing (openScopedImplication goal))
-            (throwProof (ExactProofExpectedImplicationGoal location))
-        (assumption, conclusion) <-
-            maybe
-                (throwProof (ExactProofGoalStatementMismatch location))
-                pure
-                (openScopedAssumption
-                    (Exact.preparedExactPropositionCore supplied)
-                    goal)
-        local <- allocateLocal ExactAssumption context assumption
-        PreparedAssume assumption
-            <$> prepareProof
-                fallback
-                context
-                (locals <> [local])
-                RecursiveProofInduction
-                conclusion
-                continuation
-    Raw.TakeVar location variables bound statement justification continuation -> do
-        prepareSymbolicTake
-            fallback location context locals goal variables bound statement
-            justification continuation
-    Raw.TakeNoun location nounPhrase justification continuation ->
-        prepareNounTake
-            fallback location context locals goal nounPhrase
-            justification continuation
-    Raw.BySetInduction location variable continuation ->
-        prepareSetInduction
-            fallback location context locals inductionBoundary goal
-            variable continuation
-    Raw.Have location Nothing
-            (Raw.SymbolicExists _existential variables bound statement)
-            justification continuation ->
-        prepareSymbolicTake
-            fallback location context locals goal variables bound statement
-            justification continuation
-    Raw.Have location Nothing statement justification continuation -> do
-        claim <-
-            Exact.preparedExactPropositionCore
-                <$> prepareStatement context statement
-        discharge <-
-            prepareDischarge
-                location context locals claim justification
-        local <- allocateLocal ExactDerivedClaim context claim
-        PreparedHave claim discharge
-            <$> prepareProof
-                fallback
-                context
-                (locals <> [local])
-                RecursiveProofInduction
-                goal
-                continuation
-    Raw.Have location (Just sinceStatement)
-            statement justification continuation -> do
-        sinceProposition <-
-            Exact.preparedExactPropositionCore
-                <$> prepareStatement context sinceStatement
-        claim <-
-            Exact.preparedExactPropositionCore
-                <$> prepareStatement context statement
-        (evidence, sinceLocals) <-
-            case find (localMatches sinceProposition) locals of
-                Just existing ->
-                    pure (PreparedSinceExisting existing, locals)
-                Nothing -> do
-                    discharge <-
-                        prepareDischarge
-                            location
-                            context
-                            locals
-                            sinceProposition
-                            Raw.JustificationLocal
-                    local <-
-                        allocateLocal
-                            ExactDerivedClaim context sinceProposition
-                    pure
-                        ( PreparedSinceDischarged discharge local
-                        , locals <> [local]
-                        )
-        claimDischarge <-
-            prepareDischarge
-                location context sinceLocals claim justification
-        claimLocal <-
-            allocateLocal ExactDerivedClaim context claim
-        PreparedSince
-            sinceProposition evidence claim claimDischarge
-            <$> prepareProof
-                fallback
-                context
-                (sinceLocals <> [claimLocal])
-                RecursiveProofInduction
-                goal
-                continuation
-    Raw.Suffices location statement justification continuation -> do
-        reduction <-
-            Exact.preparedExactPropositionCore
-                <$> prepareStatement context statement
-        implication <-
-            maybe
-                (impossible
-                    "a checked suffices reduction changed lexical context")
-                pure
-                (implyScopedCore reduction goal)
-        discharge <-
-            prepareDischarge
-                location context locals implication justification
-        PreparedSuffices goal reduction implication discharge
-            <$> prepareProof
-                fallback
-                context
-                locals
-                (SourceStatementInduction
-                    (claimLeadingUniversalName statement))
-                reduction
-                continuation
-    Raw.Calc location quantifier calculation continuation -> do
-        prepared <-
-            prepareCalculation
-                location context locals quantifier calculation
-        local <-
-            allocateLocal
-                ExactDerivedClaim
-                context
-                (preparedCalculationResult prepared)
-        PreparedCalculate prepared
-            <$> prepareProof
-                fallback
-                context
-                (locals <> [local])
-                RecursiveProofInduction
-                goal
-                continuation
-    Raw.Subclaim location statement subproof continuation -> do
-        claim <-
-            Exact.preparedExactPropositionCore
-                <$> prepareStatement context statement
-        preparedSubproof <-
-            prepareProof
-                location
-                context
-                locals
-                (SourceStatementInduction
-                    (claimLeadingUniversalName statement))
-                claim
-                subproof
-        local <- allocateLocal ExactDerivedClaim context claim
-        PreparedSubclaim claim preparedSubproof
-            <$> prepareProof
-                fallback
-                context
-                (locals <> [local])
-                RecursiveProofInduction
-                goal
-                continuation
-    Raw.Define location variable expression continuation -> do
-        preparedBody <-
-            liftDriver
-                (Exact.prepareExactSetExpression context expression)
-                >>= either
-                    (throwProof . ExactProofElaborationFailed)
-                    pure
-        let body = Exact.preparedExactSetExpressionCore preparedBody
-        identity <- allocateLocalIdentity
-        context' <-
-            either
-                (throwProof . ExactProofElaborationFailed)
-                pure
-                (Exact.extendExactBinderContext
-                    ((identity, variable) :| [])
-                    context)
-        case Exact.preparedExactSetExpressionConstruction preparedBody of
-            Nothing -> do
-                separationCharacteristic <-
-                    liftDriver
-                        (Declaration.currentFoundationAxiomLowering
-                            SeparationCharacteristic)
-                definition <-
-                    maybe
-                        (impossible
-                            "an exact set expression did not form a local definition")
-                        pure
-                        (scopedSetDefinition separationCharacteristic body)
-                local <-
-                    allocateLocal ExactLocalDefinition context' definition
-                PreparedDefine identity body (definition :| [])
-                    <$> prepareProof
-                        fallback context' (locals <> [local])
-                        RecursiveProofInduction
-                        (weakenCheckedScopedCore TySet goal)
-                        continuation
-            Just (Exact.PreparedUnconditionalSetConstruction construction) -> do
-                characteristics <- prepareConstructionFoundation
-                (extensional, equation) <-
-                    maybe
-                        (impossible
-                            "a checked named construction has no definition views")
-                        pure
-                        (namedSetConstructionLocalViews
-                            characteristics construction)
-                extensionalLocal <-
-                    allocateLocal
-                        ExactLocalConstructionExtensional context' extensional
-                equationLocal <-
-                    allocateLocal
-                        ExactLocalConstructionEquation context' equation
-                PreparedDefine identity body (extensional :| [equation])
-                    <$> prepareProof
-                        fallback context'
-                        (locals <> [extensionalLocal, equationLocal])
-                        RecursiveProofInduction
-                        (weakenCheckedScopedCore TySet goal)
-                        continuation
-            Just (Exact.PreparedRelationalSetConstruction construction) -> do
-                characteristics <- prepareConstructionFoundation
-                let functionality =
-                        relationalSetConstructionFunctionality construction
-                discharge <-
-                    prepareDischarge
-                        location context locals functionality
-                        Raw.JustificationEmpty
-                (extensional, equation) <-
-                    maybe
-                        (impossible
-                            "a checked relational construction has no admitted definition views")
-                        pure
-                        (relationalSetConstructionLocalViews
-                            characteristics construction functionality)
-                extensionalLocal <-
-                    allocateLocal
-                        ExactLocalConstructionExtensional context' extensional
-                equationLocal <-
-                    allocateLocal
-                        ExactLocalConstructionEquation context' equation
-                PreparedDefineRelational
-                    identity body discharge (extensional :| [equation])
-                    <$> prepareProof
-                        fallback context'
-                        (locals <> [extensionalLocal, equationLocal])
-                        RecursiveProofInduction
-                        (weakenCheckedScopedCore TySet goal)
-                        continuation
-    Raw.DefineFunction
-            location function argument value bound domain continuation -> do
-        unless (argument == bound)
-            (throwProof
-                (ExactProofLocalFunctionBinderMismatch (locate bound)))
-        when (function == argument)
-            (throwProof
-                (ExactProofLocalFunctionNameConflict (locate function)))
-        argumentIdentity <- allocateLocalIdentity
-        argumentContext <-
-            either
-                (throwProof . ExactProofElaborationFailed)
-                pure
-                (Exact.extendExactBinderContext
-                    ((argumentIdentity, argument) :| [])
-                    context)
-        graph <-
-            liftDriver
-                (Exact.prepareExactLocalFunctionGraph
-                    location context argumentContext domain value)
-                >>= either
-                    (throwProof . ExactProofElaborationFailed)
-                    pure
-        functionIdentity <- allocateLocalIdentity
-        functionContext <-
-            either
-                (throwProof . ExactProofElaborationFailed)
-                pure
-                (Exact.extendExactBinderContext
-                    ((functionIdentity, function) :| [])
-                    context)
-        replacementCharacteristic <-
-            liftDriver
-                (Declaration.currentFoundationAxiomLowering
-                    ReplacementCharacteristic)
-        definition <-
-            maybe
-                (impossible
-                    "a checked replacement graph did not form a local definition")
-                pure
-                (scopedCharacteristicDefinition
-                    replacementCharacteristic
-                    (Exact.preparedExactLocalFunctionGraphCore graph)
-                    ( Exact.preparedExactLocalFunctionGraphDomain graph
-                        :| [Exact.preparedExactLocalFunctionGraphMap graph]
-                    ))
-        local <-
-            allocateLocal ExactLocalDefinition functionContext definition
-        PreparedDefineFunction
-            functionIdentity
-            (Exact.preparedExactLocalFunctionGraphCore graph)
-            definition
-            <$> prepareProof
-                fallback
-                functionContext
-                (locals <> [local])
-                RecursiveProofInduction
-                (weakenCheckedScopedCore TySet goal)
-                continuation
-    Raw.ByCase location sourceCases ->
-        prepareByCase
-            location context locals goal sourceCases
-    Raw.ByContradiction location continuation -> do
-        let falsum = falsumScopedCore (scopedCoreContext goal)
-        negation <-
-            maybe
-                (structuralFailure
-                    location
-                    "proof by contradiction requires a proposition goal")
-                pure
-                (negateScopedCore goal)
-        local <- allocateLocal ExactAssumption context negation
-        prepared <-
-            prepareProof
-                location
-                context
-                (locals <> [local])
-                RecursiveProofInduction
-                falsum
-                continuation
-        validateStructuralComposition
-            location [goal, negation, falsum]
-            (\foundation globalType ->
-                KernelProof.validateDoubleNegationComposition
-                    foundation globalType goal negation falsum)
-        pure
-            (PreparedByContradiction
-                goal negation falsum prepared)
-    Raw.Contradiction location justification -> do
-        let falsum = falsumScopedCore (scopedCoreContext goal)
-        discharge <-
-            prepareDischarge
-                location
-                context
-                locals
-                falsum
-                justification
-        validateStructuralComposition
-            location [goal, falsum]
-            (\foundation globalType ->
-                KernelProof.validateFalsumEliminationComposition
-                    foundation globalType goal falsum)
-        pure (PreparedContradiction goal falsum discharge)
-    proof ->
-        throwProof
-            (ExactProofUnsupportedStep
-                (proofLocation fallback proof))
-  where
-    localMatches proposition
-            (PreparedLocal _ordinal _origin _support local) =
-        local == proposition
-
-prepareSetInduction
-    :: Location
-    -> Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> SetInductionBoundary
-    -> ScopedCheckedCore ObjectId
-    -> Maybe Raw.Term
-    -> Raw.Proof
-    -> Prepare PreparedProof
-prepareSetInduction
-        fallback location context locals boundary goal sourceFocus
-        continuation = do
-    selected <-
-        selectSetInductionFocus
-            location context boundary goal sourceFocus
-    case selected of
-        SelectedInitialSetInduction
-                (InitialSetInductionFocus _variable identity index) -> do
-            (foci, expectedSupport, property, antecedents, childTarget) <-
-                case boundary of
-                    InitialClaimInduction
-                            (InitialSetInductionView
-                                foundFoci support foundProperty
-                                foundAntecedents foundTarget _leadingName) ->
-                        pure
-                            ( foundFoci
-                            , support
-                            , foundProperty
-                            , foundAntecedents
-                            , foundTarget
-                            )
-                    RecursiveProofInduction ->
-                        impossible
-                            "an initial induction focus escaped its claim boundary"
-                    SourceStatementInduction _leadingName ->
-                        impossible
-                            "an initial induction focus escaped its claim boundary"
-            unless
-                ( Exact.exactBinderContextSupport context == expectedSupport
-                    && goal == childTarget
-                    && any (sameInitialFocus identity index) foci
-                )
-                (throwProof
-                    (ExactProofSetInductionGoalMismatch location))
-            PreparedSetInduction
-                <$> prepareCheckedSetInduction
-                    fallback location context locals
-                    (PreparedInitialSetInductionFocus identity index)
-                    index property antecedents childTarget continuation
-        SelectedLeadingSetInduction sourceName -> do
-            (binderType, property) <-
-                maybe
-                    (throwProof
-                        (ExactProofSetInductionGoalMismatch location))
-                    pure
-                    (openScopedForall goal)
-            unless (binderType == TySet)
-                (throwProof
-                    (ExactProofSetInductionGoalMismatch location))
-            identity <- allocateLocalIdentity
-            extendedContext <-
-                either
-                    (throwProof . ExactProofElaborationFailed)
-                    pure
-                    (case sourceName of
-                        Just variable ->
-                            Exact.extendExactBinderContext
-                                ((identity, variable) :| [])
-                                context
-                        Nothing ->
-                            Exact.extendExactAnonymousBinderContext
-                                identity context)
-            let expectedResult = weakenCheckedScopedCore TySet goal
-            prepared <- prepareCheckedSetInduction
-                fallback location extendedContext locals
-                (PreparedLeadingSetInductionFocus identity)
-                0 property [] property continuation
-            unless
-                (preparedSetInductionResult prepared == expectedResult)
-                (throwProof
-                    (ExactProofSetInductionGoalMismatch location))
-            pure (PreparedSetInduction prepared)
-  where
-    sameInitialFocus expectedIdentity expectedIndex
-            (InitialSetInductionFocus _variable identity index) =
-        identity == expectedIdentity && index == expectedIndex
-
-prepareCheckedSetInduction
-    :: Location
-    -> Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> PreparedSetInductionFocus
-    -> Natural
-    -> ScopedCheckedCore ObjectId
-    -> [ScopedCheckedCore ObjectId]
-    -> ScopedCheckedCore ObjectId
-    -> Raw.Proof
-    -> Prepare PreparedSetInduction
-prepareCheckedSetInduction
-        fallback location context locals focus selected property antecedents
-        childTarget continuation = do
-    (_predicate, hypothesis, _step, result) <-
-        maybe
-            (throwProof
-                (ExactProofSetInductionGoalMismatch location))
-            pure
-            (scopedSetInductionInstance selected property)
-    validateStructuralComposition
-        location
-        (property : hypothesis : result : childTarget : antecedents)
-        (\foundation globalType ->
-            KernelProof.validateSetInductionComposition
-                foundation globalType selected property antecedents
-                childTarget hypothesis result)
-    local <- allocateLocal ExactAssumption context hypothesis
-    child <-
-        prepareProof
-            fallback
-            context
-            (locals <> [local])
-            RecursiveProofInduction
-            childTarget
-            continuation
-    pure
-        (PreparedCheckedSetInduction
-            focus property antecedents childTarget hypothesis result child)
-
-preparedSetInductionResult
-    :: PreparedSetInduction
-    -> ScopedCheckedCore ObjectId
-preparedSetInductionResult
-        (PreparedCheckedSetInduction
-            _focus _property _antecedents _target _hypothesis result _child) =
-    result
-
-selectSetInductionFocus
-    :: Location
-    -> Exact.ExactBinderContext
-    -> SetInductionBoundary
-    -> ScopedCheckedCore ObjectId
-    -> Maybe Raw.Term
-    -> Prepare SelectedSetInductionFocus
-selectSetInductionFocus location context boundary goal sourceFocus = do
-    explicit <- traverse simpleVariable sourceFocus
-    let (initialFoci, retainedLeadingName) =
-            case boundary of
-                InitialClaimInduction
-                        (InitialSetInductionView
-                            foci _support _property _antecedents _target
-                            leadingName) ->
-                    (foci, leadingName)
-                SourceStatementInduction leadingName ->
-                    ([], leadingName)
-                RecursiveProofInduction ->
-                    ([], Nothing)
-        leadingAvailable =
-            case openScopedForall goal of
-                Just (TySet, _body) -> True
-                _ -> False
-    case explicit of
-        Just variable ->
-            case find (initialNamed variable) initialFoci of
-                Just focus ->
-                    pure (SelectedInitialSetInduction focus)
-                Nothing
-                    | leadingAvailable
-                    , isJust
-                        (Exact.exactBinderContextIndex variable context) ->
-                        throwProof
-                            (ExactProofSetInductionBinderConflict
-                                location variable)
-                    | leadingAvailable ->
-                        pure
-                            (SelectedLeadingSetInduction
-                                (Just variable))
-                    | isJust
-                        (Exact.exactBinderContextIndex variable context) ->
-                        throwProof
-                            (ExactProofSetInductionActiveBinderIneligible
-                                location variable)
-                    | otherwise ->
-                        throwProof
-                            (ExactProofSetInductionVariableNotActive
-                                location variable)
-        Nothing ->
-            case
-                ( (SelectedInitialSetInduction <$> initialFoci)
-                    <> [ SelectedLeadingSetInduction retainedLeadingName
-                       | leadingAvailable
-                       ]
-                ) of
-                [only] -> pure only
-                _ ->
-                    throwProof
-                        (ExactProofSetInductionFocusAmbiguous location)
-  where
-    simpleVariable = \case
-        Raw.TermExpr (Raw.ExprVar variable) ->
-            pure variable
-        _term ->
-            throwProof
-                (ExactProofSetInductionVariableRequired location)
-
-    initialNamed variable
-            (InitialSetInductionFocus candidate _identity _index) =
-        candidate == variable
-
-prepareByCase
-    :: Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> ScopedCheckedCore ObjectId
-    -> [Raw.Case]
-    -> Prepare PreparedProof
-prepareByCase location context locals goal sourceCases = do
-    cases <-
-        maybe
-            (throwProof (ExactProofEmptyCaseSplit location))
-            (traverse prepareCase)
-            (NonEmpty.nonEmpty sourceCases)
-    exhaustive <-
-        foldM disjoin
-            (preparedCaseAssumption (NonEmpty.head cases))
-            (preparedCaseAssumption <$> NonEmpty.tail cases)
-    discharge <-
-        prepareDischarge
-            location context locals exhaustive Raw.JustificationEmpty
-    validateStructuralComposition
-        location
-        (goal : exhaustive : (preparedCaseAssumption <$> toList cases))
-        (\foundation globalType ->
-            KernelProof.validateCaseAnalysisComposition
-                foundation
-                globalType
-                goal
-                (preparedCaseAssumption <$> cases)
-                exhaustive)
-    pure
-        (PreparedByCase
-            (PreparedCaseAnalysis goal cases exhaustive discharge))
-  where
-    prepareCase (Raw.Case statement child) = do
-        assumption <-
-            Exact.preparedExactPropositionCore
-                <$> prepareStatement context statement
-        local <- allocateLocal ExactAssumption context assumption
-        prepared <-
-            prepareProof
-                (locate statement)
-                context
-                (locals <> [local])
-                RecursiveProofInduction
-                goal
-                child
-        pure (PreparedCase assumption prepared)
-
-    disjoin left right =
-        maybe
-            (structuralFailure
-                location
-                "case assumptions changed type or lexical context")
-            pure
-            (disjoinScopedCore left right)
-
-preparedCaseAssumption
-    :: PreparedCase
-    -> ScopedCheckedCore ObjectId
-preparedCaseAssumption (PreparedCase assumption _proof) =
-    assumption
-
-preparedCaseProof :: PreparedCase -> PreparedProof
-preparedCaseProof (PreparedCase _assumption proof) =
-    proof
-
-prepareGuardedFix
-    :: Location
-    -> Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> ScopedCheckedCore ObjectId
-    -> [Exact.ExactLocalId]
-    -> ScopedCheckedCore ObjectId
-    -> Raw.Proof
-    -> Prepare PreparedProof
-prepareGuardedFix
-        fallback location context locals goal identities constraint continuation = do
-    (antecedent, conclusion) <-
-        maybe
-            (throwProof (ExactProofExpectedImplicationGoal location))
-            pure
-            (openScopedImplication goal)
-    unless (constraint == antecedent)
-        (throwProof (ExactProofGoalStatementMismatch location))
-    local <- allocateLocal ExactAssumption context constraint
-    prepared <-
-        prepareProof
-            fallback
-            context
-            (locals <> [local])
-            RecursiveProofInduction
-            conclusion
-            continuation
-    pure (PreparedFix identities (PreparedAssume constraint prepared))
-
-prepareCalculation
-    :: Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> Maybe Raw.CalcQuantifier
-    -> Raw.Calc
-    -> Prepare PreparedCalculation
-prepareCalculation location context locals quantifier calculation = do
-    (identities, calculationContext, calculationGuard) <-
-        prepareCalculationScope context quantifier
-    case calculation of
-        Raw.Equation first destinations -> do
-            firstChecked <- prepareSetEndpoint calculationContext first
-            checkedDestinations <-
-                traverse
-                    (\(destination, justification) -> do
-                        checked <-
-                            prepareSetEndpoint calculationContext destination
-                        pure
-                            ( locate destination
-                            , checked
-                            , justification
-                            ))
-                    destinations
-            finishCalculation
-                location context locals TySet identities calculationGuard
-                firstChecked checkedDestinations
-        Raw.Biconditionals first destinations -> do
-            firstChecked <- preparePropositionEndpoint calculationContext first
-            checkedDestinations <-
-                traverse
-                    (\(destination, justification) -> do
-                        checked <-
-                            preparePropositionEndpoint
-                                calculationContext destination
-                        pure
-                            ( locate destination
-                            , checked
-                            , justification
-                            ))
-                    destinations
-            finishCalculation
-                location context locals TyProp identities calculationGuard
-                firstChecked checkedDestinations
-  where
-    prepareSetEndpoint endpointContext expression =
-        Exact.preparedExactSetExpressionCore
-            <$> ( liftDriver
-                    (Exact.prepareExactSetExpression
-                        endpointContext expression)
-                    >>= either
-                        (throwProof . ExactProofElaborationFailed)
-                        pure
-                )
-
-    preparePropositionEndpoint endpointContext formula =
-        Exact.preparedExactPropositionCore
-            <$> prepareStatement endpointContext (Raw.StmtFormula formula)
-
-prepareCalculationScope
-    :: Exact.ExactBinderContext
-    -> Maybe Raw.CalcQuantifier
-    -> Prepare
-        ( [Exact.ExactLocalId]
-        , Exact.ExactBinderContext
-        , Maybe (ScopedCheckedCore ObjectId)
-        )
-prepareCalculationScope context = \case
-    Nothing ->
-        pure ([], context, Nothing)
-    Just (Raw.CalcQuantifier variables bound suchThat) -> do
-        identities <- traverse (const allocateLocalIdentity) variables
-        calculationContext <-
-            either
-                (throwProof . ExactProofElaborationFailed)
-                pure
-                (Exact.extendExactBinderContext
-                    (NonEmpty.zip identities variables)
-                    context)
-        boundGuard <-
-            prepareSymbolicBoundConstraints
-                calculationContext variables bound
-        suchThatGuard <-
-            traverse
-                (fmap Exact.preparedExactPropositionCore
-                    . prepareStatement calculationContext)
-                suchThat
-        calculationGuard <-
-            normalizeCalculationGuard
-                (boundGuard : maybeToList suchThatGuard)
-        pure (toList identities, calculationContext, calculationGuard)
-
-normalizeCalculationGuard
-    :: [ScopedCheckedCore ObjectId]
-    -> Prepare (Maybe (ScopedCheckedCore ObjectId))
-normalizeCalculationGuard guards =
-    foldM add Nothing guards
-  where
-    add accumulated constraint
-        | isScopedTruth constraint = pure accumulated
-        | otherwise =
-            case accumulated of
-                Nothing -> pure (Just constraint)
-                Just previous ->
-                    Just
-                        <$> maybe
-                            (impossible
-                                "checked calculation guards changed context")
-                            pure
-                            (conjoinScopedCore previous constraint)
-
-    isScopedTruth proposition =
-        scopedCoreType proposition == TyProp
-            && scopedCoreTerm proposition == CImp CFalsum CFalsum
-
-finishCalculation
-    :: Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> CoreType
-    -> [Exact.ExactLocalId]
-    -> Maybe (ScopedCheckedCore ObjectId)
-    -> ScopedCheckedCore ObjectId
-    -> NonEmpty
-        ( Location
-        , ScopedCheckedCore ObjectId
-        , Raw.Justification
-        )
-    -> Prepare PreparedCalculation
-finishCalculation
-        fallback context locals operandType identities calculationGuard
-        first destinations = do
-    links <- prepareCalculationLinks first destinations
-    let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links)
-    resultOpen <-
-        calculationEquality first finalEndpoint
-    result <-
-        closeCalculationProposition identities calculationGuard resultOpen
-    pure
-        (PreparedCheckedCalculation
-            operandType identities calculationGuard first links result)
-  where
-    prepareCalculationLinks previous (destination :| rest) = do
-        (next, firstLink) <- prepareCalculationLink previous destination
-        later <- prepareRemainingCalculationLinks next rest
-        pure (firstLink :| later)
-
-    prepareRemainingCalculationLinks _previous [] =
-        pure []
-    prepareRemainingCalculationLinks previous (destination : rest) = do
-        (next, link) <- prepareCalculationLink previous destination
-        (link :) <$> prepareRemainingCalculationLinks next rest
-
-    prepareCalculationLink previous
-            (destinationLocation, destination, justification) = do
-            linkOpen <- calculationEquality previous destination
-            link <- closeCalculationProposition
-                identities calculationGuard linkOpen
-            discharge <-
-                prepareDischarge
-                    (if destinationLocation == Nowhere
-                        then fallback
-                        else destinationLocation)
-                    context
-                    locals
-                    link
-                    justification
-            pure
-                ( destination
-                , PreparedCalculationLink destination discharge
-                )
-
-    calculationEquality left right =
-        maybe
-            (impossible
-                "checked calculation endpoints changed type or context")
-            pure
-            (equalScopedCore left right)
-
-closeCalculationProposition
-    :: [Exact.ExactLocalId]
-    -> Maybe (ScopedCheckedCore ObjectId)
-    -> ScopedCheckedCore ObjectId
-    -> Prepare (ScopedCheckedCore ObjectId)
-closeCalculationProposition identities calculationGuard proposition = do
-    guarded <-
-        case calculationGuard of
-            Nothing -> pure proposition
-            Just constraint ->
-                maybe
-                    (impossible
-                        "a checked calculation guard changed context")
-                    pure
-                    (implyScopedCore constraint proposition)
-    pure (closeBinders (length identities) guarded)
-  where
-    closeBinders 0 closed = closed
-    closeBinders remaining open =
-        closeBinders (remaining - 1)
-            (fromMaybe
-                (impossible
-                    "a checked calculation lost a quantified binder")
-                (closeScopedForall open))
-
-preparedCalculationResult
-    :: PreparedCalculation
-    -> ScopedCheckedCore ObjectId
-preparedCalculationResult
-        (PreparedCheckedCalculation
-            _operandType _identities _guard _first _links result) =
-    result
-
-preparedCalculationLinkDestination
-    :: PreparedCalculationLink
-    -> ScopedCheckedCore ObjectId
-preparedCalculationLinkDestination
-        (PreparedCalculationLink destination _discharge) =
-    destination
-
-preparedCalculationLinkDischarge
-    :: PreparedCalculationLink
-    -> PreparedDischarge
-preparedCalculationLinkDischarge
-        (PreparedCalculationLink _destination discharge) =
-    discharge
-
-preparedDischargeGoal
-    :: PreparedDischarge
-    -> ScopedCheckedCore ObjectId
-preparedDischargeGoal = \case
-    PreparedVampireDischarge _location _justification goal _obligation ->
-        goal
-    PreparedSetExtensionality _location goal ->
-        goal
-
-prepareSymbolicBoundConstraints
-    :: Exact.ExactBinderContext
-    -> NonEmpty Raw.VarSymbol
-    -> Raw.Bound
-    -> Prepare (ScopedCheckedCore ObjectId)
-prepareSymbolicBoundConstraints context variables bound =
-    Exact.preparedExactPropositionCore
-        <$> ( liftDriver
-                (Exact.prepareExactSymbolicBoundConstraints
-                    context variables bound)
-                >>= either
-                    (throwProof . ExactProofElaborationFailed)
-                    pure
-            )
-
-prepareSymbolicTake
-    :: Location
-    -> Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> ScopedCheckedCore ObjectId
-    -> NonEmpty Raw.VarSymbol
-    -> Raw.Bound
-    -> Raw.Stmt
-    -> Raw.Justification
-    -> Raw.Proof
-    -> Prepare PreparedProof
-prepareSymbolicTake
-        fallback location context locals goal variables bound statement
-        justification continuation = do
-    identities <- traverse (const allocateLocalIdentity) variables
-    context' <-
-        either
-            (throwProof . ExactProofElaborationFailed)
-            pure
-            (Exact.extendExactBinderContext
-                (NonEmpty.zip identities variables)
-                context)
-    witness <-
-        Exact.preparedExactPropositionCore
-            <$> ( liftDriver
-                    (Exact.prepareExactSymbolicWitnessConstraints
-                        context' variables bound statement)
-                    >>= either
-                        (throwProof . ExactProofElaborationFailed)
-                        pure
-                )
-    prepareTake
-        fallback location context locals goal context'
-        (toList identities) witness justification continuation
-
-prepareNounTake
-    :: Location
-    -> Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> ScopedCheckedCore ObjectId
-    -> Raw.NounPhrase []
-    -> Raw.Justification
-    -> Raw.Proof
-    -> Prepare PreparedProof
-prepareNounTake
-        fallback location context locals goal nounPhrase
-        justification continuation = do
-    (identities, context') <-
-        case nounPhrase of
-            Raw.NounPhrase _left _noun variables _right _suchThat ->
-                case NonEmpty.nonEmpty variables of
-                    Just binders -> do
-                        identities <-
-                            traverse (const allocateLocalIdentity) binders
-                        context' <-
-                            either
-                                (throwProof . ExactProofElaborationFailed)
-                                pure
-                                (Exact.extendExactBinderContext
-                                    (NonEmpty.zip identities binders)
-                                    context)
-                        pure (toList identities, context')
-                    Nothing -> do
-                        identity <- allocateLocalIdentity
-                        context' <-
-                            either
-                                (throwProof . ExactProofElaborationFailed)
-                                pure
-                                (Exact.extendExactAnonymousBinderContext
-                                    identity context)
-                        pure ([identity], context')
-    witness <-
-        Exact.preparedExactPropositionCore
-            <$> ( liftDriver
-                    (Exact.prepareExactNounWitnessConstraints
-                        context' nounPhrase)
-                    >>= either
-                        (throwProof . ExactProofElaborationFailed)
-                        pure
-                )
-    prepareTake
-        fallback location context locals goal context'
-        identities witness justification continuation
-
-prepareTake
-    :: Location
-    -> Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> ScopedCheckedCore ObjectId
-    -> Exact.ExactBinderContext
-    -> [Exact.ExactLocalId]
-    -> ScopedCheckedCore ObjectId
-    -> Raw.Justification
-    -> Raw.Proof
-    -> Prepare PreparedProof
-prepareTake
-        fallback location context locals goal witnessContext
-        identities witness justification continuation = do
-    let witnessCount = length identities
-        existence = closeTakenWitnesses witnessCount witness
-        goal' = weakenForTakenWitnesses witnessCount goal
-    discharge <-
-        prepareDischarge
-            location context locals existence justification
-    local <- allocateLocal ExactAssumption witnessContext witness
-    PreparedTake identities witness discharge
-        <$> prepareProof
-            fallback
-            witnessContext
-            (locals <> [local])
-            RecursiveProofInduction
-            goal'
-            continuation
-
--- The discharged existential and the opened witness premise are the same
--- checked proposition viewed on opposite sides of existential elimination.
-closeTakenWitnesses
-    :: Int
-    -> ScopedCheckedCore ObjectId
-    -> ScopedCheckedCore ObjectId
-closeTakenWitnesses binderCount = go binderCount
-  where
-    go 0 proposition = proposition
-    go remaining proposition =
-        go (remaining - 1)
-            (fromMaybe
-                (impossible "a taken witness has no checked binder")
-                (closeScopedExists proposition))
-
-weakenForTakenWitnesses
-    :: Int
-    -> ScopedCheckedCore ObjectId
-    -> ScopedCheckedCore ObjectId
-weakenForTakenWitnesses binderCount = go binderCount
-  where
-    go 0 proposition = proposition
-    go remaining proposition =
-        go (remaining - 1)
-            (weakenCheckedScopedCore TySet proposition)
-
-openFixedVariables
-    :: Exact.ExactBinderContext
-    -> ScopedCheckedCore ObjectId
-    -> NonEmpty Raw.VarSymbol
-    -> Prepare
-        ( Exact.ExactBinderContext
-        , ScopedCheckedCore ObjectId
-        , [Exact.ExactLocalId]
-        )
-openFixedVariables initialContext initialGoal variables =
-    foldM openOne
-        (initialContext, initialGoal, [])
-        (toList variables)
-  where
-    openOne (context, goal, identities) variable = do
-        (binderType, body) <-
-            maybe
-                (throwProof
-                    (ExactProofExpectedUniversalGoal
-                        (locate variable)))
-                pure
-                (openScopedForall goal)
-        unless (binderType == TySet)
-            (throwProof
-                (ExactProofExpectedUniversalGoal
-                    (locate variable)))
-        identity <- allocateLocalIdentity
-        context' <-
-            either
-                (throwProof . ExactProofElaborationFailed)
-                pure
-                (Exact.extendExactBinderContext
-                    ((identity, variable) :| [])
-                    context)
-        pure (context', body, identities <> [identity])
-
-allocateLocalIdentity :: Prepare Exact.ExactLocalId
-allocateLocalIdentity = do
-    state <- State.get
-    State.put
-        state
-            { prepareNextLocal = prepareNextLocal state + 1
-            }
-    pure (Exact.exactLocalId (prepareNextLocal state))
-
-allocateLocal
-    :: ExactLocalOrigin
-    -> Exact.ExactBinderContext
-    -> ScopedCheckedCore ObjectId
-    -> Prepare PreparedLocal
-allocateLocal origin context proposition = do
-    state <- State.get
-    State.put
-        state
-            { prepareNextPremise = prepareNextPremise state + 1
-            }
-    pure
-        (PreparedLocal
-            (Backend.localPremiseOrdinal
-                (prepareNextPremise state))
-            origin
-            (Exact.exactBinderContextSupport context)
-            proposition)
-
-prepareConstructionFoundation
-    :: Prepare SetConstructionFoundation
-prepareConstructionFoundation = do
-    familyUnion <- foundation FamilyUnionCharacteristic
-    separation <- foundation SeparationCharacteristic
-    replacement <- foundation ReplacementCharacteristic
-    setChoose <- foundation SetChooseWitness
-    pure
-        (setConstructionFoundation
-            familyUnion separation replacement setChoose)
-  where
-    foundation tag =
-        liftDriver
-            (Declaration.currentFoundationAxiomLowering tag)
-
-prepareDischarge
-    :: Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> ScopedCheckedCore ObjectId
-    -> Raw.Justification
-    -> Prepare PreparedDischarge
-prepareDischarge location context locals goal justification =
-    prepareDischargeWith
-        (dischargeModeFor goal)
-        [] Nothing location context locals goal justification
-
--- A contradictory-axioms answer can establish falsum, but never an unrelated
--- proposition directly. Derive that distinction from the checked target so
--- every surface proof spelling reaches the same guarded request path.
-dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode
-dischargeModeFor goal
-    | scopedCoreType goal == TyProp
-    , scopedCoreTerm goal == CFalsum =
-        IndirectContradictionDischarge
-    | otherwise =
-        DirectDischarge
-
-data DischargeMode
-    = DirectDischarge
-    | IndirectContradictionDischarge
-
-prepareDischargeWith
-    :: DischargeMode
-    -> [FoundationAxiomTag]
-    -> Maybe Declaration.VampirePremiseSelection
-    -> Location
-    -> Exact.ExactBinderContext
-    -> [PreparedLocal]
-    -> ScopedCheckedCore ObjectId
-    -> Raw.Justification
-    -> Prepare PreparedDischarge
-prepareDischargeWith
-        dischargeMode auxiliaries selectionOverride
-        location context locals goal justification =
-    case justification of
-        Raw.JustificationSetExt -> do
-            (leftToRight, rightToLeft) <-
-                maybe
-                    (throwProof
-                        (ExactProofSetExtensionalityGoalMismatch location))
-                    pure
-                    (splitScopedSetEquality goal)
-            unless
-                ( hasDerivedLocal leftToRight
-                    && hasDerivedLocal rightToLeft
-                )
-                (throwProof
-                    (ExactProofSetExtensionalityDirectionsUnavailable
-                        location))
-            pure (PreparedSetExtensionality location goal)
-        _ -> do
-            preparedJustification <-
-                prepareJustification location justification
-            prepared <-
-                liftDriver
-                    (prepareObligation
-                        (Exact.exactBinderContextSupport context)
-                        goal
-                        (toScopedPremise <$> locals)
-                        auxiliaries
-                        (fromMaybe
-                            (vampirePremiseSelection preparedJustification)
-                            selectionOverride))
-                    >>= either
-                        (throwProof
-                            . ExactProofObligationPreparationFailed location)
-                        pure
-            pure
-                (PreparedVampireDischarge
-                    location
-                    preparedJustification
-                    goal
-                    prepared)
-  where
-    prepareObligation =
-        case dischargeMode of
-            DirectDischarge ->
-                Declaration.prepareScopedVampireObligationLowering
-            IndirectContradictionDischarge ->
-                Declaration.prepareScopedContradictionObligationLowering
-
-    hasDerivedLocal proposition =
-        any
-            (\case
-                PreparedLocal
-                        _ordinal ExactDerivedClaim _support local ->
-                    local == proposition
-                PreparedLocal{} ->
-                    False)
-            locals
-
-    toScopedPremise
-            (PreparedLocal ordinal origin support proposition) =
-        Declaration.scopedVampirePremise
-            ordinal origin support proposition
-
-prepareJustification
-    :: Location
-    -> Raw.Justification
-    -> Prepare PreparedJustification
-prepareJustification _location Raw.JustificationEmpty =
-    pure PreparedAuto
-prepareJustification location (Raw.JustificationRef markers) = do
-    resolved <- traverse (resolveReference location) (toList markers)
-    let unique = stableUnique resolved
-    case unique of
-        [] ->
-            impossible "a nonempty citation list resolved to no facts"
-        first : rest ->
-            pure (PreparedReferences (first :| rest))
-prepareJustification _location Raw.JustificationLocal =
-    pure PreparedLocalOnly
-prepareJustification location Raw.JustificationSetExt =
-    throwProof (ExactProofUnsupportedStep location)
-
-vampirePremiseSelection
-    :: PreparedJustification
-    -> Declaration.VampirePremiseSelection
-vampirePremiseSelection = \case
-    PreparedAuto ->
-        Declaration.VampireImplicitPremises
-    PreparedReferences fingerprints ->
-        Declaration.VampireExplicitPremises fingerprints
-    PreparedLocalOnly ->
-        Declaration.VampireLocalPremises
-
-resolveReference
-    :: Location
-    -> Raw.Marker
-    -> Prepare SemanticFactOccurrenceFingerprint
-resolveReference location marker@(Raw.Marker name) = do
-    resolved <-
-        liftDriver
-            (Declaration.resolveVisibleFactAliasLowering
-                (semanticName name))
-    maybe
-        (throwProof
-            (ExactProofUnknownReference location marker))
-        pure
-        resolved
-
-prepareStatement
-    :: Exact.ExactBinderContext
-    -> Raw.Stmt
-    -> Prepare Exact.PreparedExactProposition
-prepareStatement context statement =
-    liftDriver
-        (Exact.prepareExactProposition context statement)
-        >>= either
-            (throwProof . ExactProofElaborationFailed)
-            pure
-
-validateStructuralComposition
-    :: Location
-    -> [ScopedCheckedCore ObjectId]
-    -> ( CheckedFoundation
-         -> (ObjectId -> Maybe CoreType)
-         -> Either KernelProof.KernelProofBuildError ()
-       )
-    -> Prepare ()
-validateStructuralComposition location propositions validate = do
-    foundation <-
-        liftDriver Declaration.currentFoundationLowering
-    let identities =
-            Set.toAscList
-                (Set.unions
-                    ( canonicalTermGlobals . scopedCoreTerm
-                        <$> propositions
-                    ))
-    types <-
-        traverse
-            (\identity -> do
-                coreType <-
-                    liftDriver
-                        (Declaration.objectTypeLowering identity)
-                maybe
-                    (impossible
-                        "a checked structural proof lost a global object")
-                    (\availableType -> pure (identity, availableType))
-                    coreType)
-            identities
-    either
-        (throwProof
-            . ExactProofStructuralCompositionFailed location)
-        pure
-        (validate foundation
-            (\identity -> Map.lookup identity (Map.fromList types)))
-
-structuralFailure :: Location -> Text -> Prepare value
-structuralFailure location message =
-    throwProof
-        (ExactProofStructuralCompositionFailed
-            location
-            (KernelProof.ProofStructuralCompositionMismatch message))
-
-data CheckedExactProofAuthorization = CheckedExactProofAuthorization
-    !PreparedProof
-    !Bool
-
-lowerPreparedExactProof
-    :: PreparedExactProof
-    -> Declaration.LoweringDriver
-        (Either
-            Declaration.DeclarationError
-            (Declaration.CheckedDeclaration CheckedExactProofAuthorization))
-lowerPreparedExactProof
-        (PreparedExactProof _location alias target proof syntax) =
-    fmap checked
-        <$> Declaration.prepareCandidateSpecLowering
-            [] target SearchEligible [alias]
-  where
-    checked spec =
-        Declaration.checkedProofDeclaration
-            syntax [] [] [] []
-            [Declaration.checkedCandidate spec planning :| []]
-            (CheckedExactProofAuthorization
-                proof
-                (isJust (preparedProofFirstOmission proof)))
-      where
-        requests = plannedProofRequests proof
-        planning
-            | isJust (preparedProofFirstOmission proof) =
-                Declaration.checkedOmittedPlanning requests []
-            | otherwise =
-                Declaration.checkedSourceProofPlanning requests []
-
-authorizeCheckedExactProof
-    :: CheckedExactProofAuthorization
-    -> [NonEmpty Declaration.ReservedCandidate]
-    -> Declaration.Declaration ()
-authorizeCheckedExactProof
-        (CheckedExactProofAuthorization proof hasOmission) = \case
-    [candidate :| []]
-        | hasOmission ->
-            Declaration.authorizeOmittedCandidate
-                candidate
-                (executePreparedProof proof)
-        | otherwise ->
-            Declaration.authorizeVampireCandidate
-                candidate
-                (executePreparedProof proof)
-    stages ->
-        Declaration.failDeclaration
-            (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                1 (length stages))
-
-data CheckedFinalPreludeFoundationAuthorization =
-    CheckedFinalPreludeFoundationAuthorization !FoundationAxiomTag
-
-lowerPreparedFinalPreludeFoundationClaim
-    :: PreparedFinalPreludeFoundationClaim
-    -> Declaration.LoweringDriver
-        (Either
-            Declaration.DeclarationError
-            (Declaration.CheckedDeclaration
-                CheckedFinalPreludeFoundationAuthorization))
-lowerPreparedFinalPreludeFoundationClaim
-        (PreparedFinalPreludeFoundationClaim
-            _location alias target tag syntax) =
-    fmap checked
-        <$> Declaration.prepareCandidateSpecLowering
-            [] target SearchEligible [alias]
-  where
-    checked spec =
-        Declaration.checkedProofDeclaration
-            syntax [] [] [] []
-            [ Declaration.checkedCandidate spec
-                (Declaration.checkedKernelPlanning
-                    (Authority.FoundationLeaf tag) [])
-                :| []
-            ]
-            (CheckedFinalPreludeFoundationAuthorization tag)
-
-authorizeCheckedFinalPreludeFoundationClaim
-    :: CheckedFinalPreludeFoundationAuthorization
-    -> [NonEmpty Declaration.ReservedCandidate]
-    -> Declaration.Declaration ()
-authorizeCheckedFinalPreludeFoundationClaim
-        (CheckedFinalPreludeFoundationAuthorization tag) = \case
-    [candidate :| []] ->
-        Declaration.authorizeKernelConstructionCandidate
-            (Authority.FoundationLeaf tag)
-            candidate
-            (pure (foundationFactDerivation tag))
-    stages ->
-        Declaration.failDeclaration
-            (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                1 (length stages))
-
-preparedProofFirstOmission :: PreparedProof -> Maybe Location
-preparedProofFirstOmission = \case
-    PreparedImplicitAuto{} -> Nothing
-    PreparedQed{} -> Nothing
-    PreparedOmitted location _goal -> Just location
-    PreparedFix _identities continuation ->
-        preparedProofFirstOmission continuation
-    PreparedAssume _antecedent continuation ->
-        preparedProofFirstOmission continuation
-    PreparedTake _identities _witness _discharge continuation ->
-        preparedProofFirstOmission continuation
-    PreparedSetInduction
-            (PreparedCheckedSetInduction
-                _focus _property _antecedents _target
-                _hypothesis _result child) ->
-        preparedProofFirstOmission child
-    PreparedHave _claim _discharge continuation ->
-        preparedProofFirstOmission continuation
-    PreparedSuffices _goal _reduction _implication _discharge continuation ->
-        preparedProofFirstOmission continuation
-    PreparedCalculate _calculation continuation ->
-        preparedProofFirstOmission continuation
-    PreparedSince _since _evidence _claim _discharge continuation ->
-        preparedProofFirstOmission continuation
-    PreparedSubclaim _claim subproof continuation ->
-        preparedProofFirstOmission subproof
-            <|> preparedProofFirstOmission continuation
-    PreparedDefine _identity _body _definition continuation ->
-        preparedProofFirstOmission continuation
-    PreparedDefineRelational
-            _identity _body _functionality _definitions continuation ->
-        preparedProofFirstOmission continuation
-    PreparedDefineFunction _identity _graph _definition continuation ->
-        preparedProofFirstOmission continuation
-    PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) ->
-        foldr
-            ((<|>) . preparedProofFirstOmission . preparedCaseProof)
-            Nothing
-            cases
-    PreparedByContradiction _goal _negation _falsum child ->
-        preparedProofFirstOmission child
-    PreparedContradiction{} -> Nothing
-
-plannedProofRequests
-    :: PreparedProof
-    -> [Declaration.CheckedPlannedVampireRequest]
-plannedProofRequests = \case
-    PreparedImplicitAuto discharge -> plannedDischargeRequests discharge
-    PreparedQed discharge -> plannedDischargeRequests discharge
-    PreparedOmitted{} -> []
-    PreparedFix _identities continuation ->
-        plannedProofRequests continuation
-    PreparedAssume _antecedent continuation ->
-        plannedProofRequests continuation
-    PreparedTake _identities _witness discharge continuation ->
-        plannedDischargeRequests discharge <> plannedProofRequests continuation
-    PreparedSetInduction
-            (PreparedCheckedSetInduction
-                _focus _property _antecedents _target
-                _hypothesis _result child) ->
-        plannedProofRequests child
-    PreparedHave _claim discharge continuation ->
-        plannedDischargeRequests discharge <> plannedProofRequests continuation
-    PreparedSuffices _goal _reduction _implication discharge continuation ->
-        plannedDischargeRequests discharge <> plannedProofRequests continuation
-    PreparedCalculate calculation continuation ->
-        plannedCalculationRequests calculation
-            <> plannedProofRequests continuation
-    PreparedSince _since evidence _claim discharge continuation ->
-        plannedSinceEvidenceRequests evidence
-            <> plannedDischargeRequests discharge
-            <> plannedProofRequests continuation
-    PreparedSubclaim _claim subproof continuation ->
-        plannedProofRequests subproof <> plannedProofRequests continuation
-    PreparedDefine _identity _body _definition continuation ->
-        plannedProofRequests continuation
-    PreparedDefineRelational
-            _identity _body functionality _definitions continuation ->
-        plannedDischargeRequests functionality
-            <> plannedProofRequests continuation
-    PreparedDefineFunction _identity _graph _definition continuation ->
-        plannedProofRequests continuation
-    PreparedByCase
-            (PreparedCaseAnalysis _goal cases _exhaustive discharge) ->
-        concatMap
-            (plannedProofRequests . preparedCaseProof)
-            (toList cases)
-            <> plannedDischargeRequests discharge
-    PreparedByContradiction _goal _negation _falsum child ->
-        plannedProofRequests child
-    PreparedContradiction _goal _falsum discharge ->
-        plannedDischargeRequests discharge
-
-plannedDischargeRequests
-    :: PreparedDischarge
-    -> [Declaration.CheckedPlannedVampireRequest]
-plannedDischargeRequests = \case
-    PreparedVampireDischarge location _justification _goal obligation ->
-        [Declaration.checkedPlannedVampireRequest location obligation]
-    PreparedSetExtensionality{} -> []
-
-plannedCalculationRequests
-    :: PreparedCalculation
-    -> [Declaration.CheckedPlannedVampireRequest]
-plannedCalculationRequests
-        (PreparedCheckedCalculation
-            _operandType _identities _guard _first links _result) =
-    concatMap
-        (plannedDischargeRequests . preparedCalculationLinkDischarge)
-        (toList links)
-
-plannedSinceEvidenceRequests
-    :: PreparedSinceEvidence
-    -> [Declaration.CheckedPlannedVampireRequest]
-plannedSinceEvidenceRequests = \case
-    PreparedSinceExisting{} -> []
-    PreparedSinceDischarged discharge _local ->
-        plannedDischargeRequests discharge
-
-executePreparedProof
-    :: PreparedProof
-    -> Declaration.CandidateProof ()
-executePreparedProof = \case
-    PreparedImplicitAuto discharge ->
-        executeDischarge discharge
-    PreparedQed discharge ->
-        executeDischarge discharge
-    PreparedOmitted _location _goal ->
-        Declaration.recordOmittedUse
-    PreparedFix _identities continuation ->
-        executePreparedProof continuation
-    PreparedAssume _antecedent continuation ->
-        executePreparedProof continuation
-    PreparedTake _identities _witness discharge continuation -> do
-        executeDischarge discharge
-        executePreparedProof continuation
-    PreparedSetInduction
-            (PreparedCheckedSetInduction
-                _focus _property _antecedents _target
-                _hypothesis _result child) ->
-        executePreparedProof child
-    PreparedHave _claim discharge continuation -> do
-        executeDischarge discharge
-        executePreparedProof continuation
-    PreparedSuffices goal reduction implication discharge continuation -> do
-        executeDischarge discharge
-        executePreparedProof continuation
-        unless
-            (implyScopedCore reduction goal == Just implication)
-            (impossible "a prepared suffices implication diverged")
-    PreparedCalculate calculation continuation -> do
-        executePreparedCalculation calculation
-        executePreparedProof continuation
-    PreparedSince sinceProposition evidence _claim discharge continuation -> do
-        executeSinceEvidence sinceProposition evidence
-        executeDischarge discharge
-        executePreparedProof continuation
-    PreparedSubclaim _claim subproof continuation -> do
-        executePreparedProof subproof
-        executePreparedProof continuation
-    PreparedDefine _identity _body _definition continuation ->
-        executePreparedProof continuation
-    PreparedDefineRelational
-            _identity _body functionality _definitions continuation -> do
-        executeDischarge functionality
-        executePreparedProof continuation
-    PreparedDefineFunction _identity _graph _definition continuation ->
-        executePreparedProof continuation
-    PreparedByCase
-            (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do
-        traverse_ (executePreparedProof . preparedCaseProof) cases
-        executeDischarge discharge
-    PreparedByContradiction _goal _negation _falsum child ->
-        executePreparedProof child
-    PreparedContradiction _goal _falsum discharge ->
-        executeDischarge discharge
-
-executeDischarge
-    :: PreparedDischarge
-    -> Declaration.CandidateProof ()
-executeDischarge
-        (PreparedVampireDischarge
-            location _justification _goal obligation) =
-    Declaration.locateProofObligation location
-        (Declaration.acceptPreparedVampireObligation obligation)
-executeDischarge PreparedSetExtensionality{} =
-    pure ()
-
-executePreparedCalculation
-    :: PreparedCalculation
-    -> Declaration.CandidateProof ()
-executePreparedCalculation
-        (PreparedCheckedCalculation
-            _operandType _identities _guard _first links _result) =
-    traverse_
-        (executeDischarge . preparedCalculationLinkDischarge)
-        links
-
-executeSinceEvidence
-    :: ScopedCheckedCore ObjectId
-    -> PreparedSinceEvidence
-    -> Declaration.CandidateProof ()
-executeSinceEvidence proposition = \case
-    PreparedSinceExisting local ->
-        unless (preparedLocalProposition local == proposition)
-            (impossible "a structural since premise diverged")
-    PreparedSinceDischarged discharge local -> do
-        executeDischarge discharge
-        unless
-            ( preparedDischargeGoal discharge == proposition
-                && preparedLocalProposition local == proposition
-            )
-            (impossible "a discharged since premise diverged")
-
-preparedLocalProposition
-    :: PreparedLocal
-    -> ScopedCheckedCore ObjectId
-preparedLocalProposition
-        (PreparedLocal _ordinal _origin _support proposition) =
-    proposition
-
-encodePreparedProof :: PreparedProof -> ByteString
-encodePreparedProof =
-    encodeCache . putPreparedProof
-
-putPreparedProof :: PreparedProof -> CachePut
-putPreparedProof = \case
-    PreparedImplicitAuto discharge -> do
-        putCacheTag 0x00
-        putPreparedDischarge discharge
-    PreparedQed discharge -> do
-        putCacheTag 0x01
-        putPreparedDischarge discharge
-    PreparedOmitted _location goal -> do
-        putCacheTag 0x06
-        putScopedProposition goal
-    PreparedFix identities continuation -> do
-        putCacheTag 0x02
-        putCacheList
-            (putCacheNatural . Exact.exactLocalIdValue)
-            identities
-        putPreparedProof continuation
-    PreparedAssume antecedent continuation -> do
-        putCacheTag 0x03
-        putScopedProposition antecedent
-        putPreparedProof continuation
-    PreparedTake identities witness discharge continuation -> do
-        putCacheTag 0x08
-        putCacheList
-            (putCacheNatural . Exact.exactLocalIdValue)
-            identities
-        putScopedProposition witness
-        putPreparedDischarge discharge
-        putPreparedProof continuation
-    PreparedSetInduction
-            (PreparedCheckedSetInduction
-                focus property antecedents target hypothesis result child) -> do
-        putCacheTag 0x07
-        putPreparedSetInductionFocus focus
-        putScopedProposition property
-        putCacheList putScopedProposition antecedents
-        putScopedProposition target
-        putScopedProposition hypothesis
-        putScopedProposition result
-        putPreparedProof child
-    PreparedHave claim discharge continuation -> do
-        putCacheTag 0x04
-        putScopedProposition claim
-        putPreparedDischarge discharge
-        putPreparedProof continuation
-    PreparedSuffices goal reduction implication discharge continuation -> do
-        putCacheTag 0x0c
-        putScopedProposition goal
-        putScopedProposition reduction
-        putScopedProposition implication
-        putPreparedDischarge discharge
-        putPreparedProof continuation
-    PreparedCalculate calculation continuation -> do
-        putCacheTag 0x0d
-        putPreparedCalculation calculation
-        putPreparedProof continuation
-    PreparedSince sinceProposition evidence claim discharge continuation -> do
-        putCacheTag 0x0e
-        putScopedProposition sinceProposition
-        putPreparedSinceEvidence evidence
-        putScopedProposition claim
-        putPreparedDischarge discharge
-        putPreparedProof continuation
-    PreparedSubclaim claim subproof continuation -> do
-        putCacheTag 0x05
-        putScopedProposition claim
-        putPreparedProof subproof
-        putPreparedProof continuation
-    PreparedDefine identity body definitions continuation -> do
-        putCacheTag 0x09
-        putCacheNatural (Exact.exactLocalIdValue identity)
-        putScopedTerm body
-        putCacheList putScopedProposition (toList definitions)
-        putPreparedProof continuation
-    PreparedDefineRelational
-            identity body functionality definitions continuation -> do
-        putCacheTag 0x11
-        putCacheNatural (Exact.exactLocalIdValue identity)
-        putScopedTerm body
-        putPreparedDischarge functionality
-        putCacheList putScopedProposition (toList definitions)
-        putPreparedProof continuation
-    PreparedByCase caseAnalysis -> do
-        putCacheTag 0x0f
-        putPreparedCaseAnalysis caseAnalysis
-    PreparedByContradiction goal negation falsum child -> do
-        putCacheTag 0x10
-        putScopedProposition goal
-        putScopedProposition negation
-        putScopedProposition falsum
-        putPreparedProof child
-    PreparedContradiction goal falsum discharge -> do
-        putCacheTag 0x0a
-        putScopedProposition goal
-        putScopedProposition falsum
-        putPreparedDischarge discharge
-    PreparedDefineFunction identity graph definition continuation -> do
-        putCacheTag 0x0b
-        putCacheNatural (Exact.exactLocalIdValue identity)
-        putScopedTerm graph
-        putScopedProposition definition
-        putPreparedProof continuation
-
-putPreparedSetInductionFocus
-    :: PreparedSetInductionFocus
-    -> CachePut
-putPreparedSetInductionFocus = \case
-    PreparedInitialSetInductionFocus identity index -> do
-        putCacheTag 0x00
-        putCacheNatural (Exact.exactLocalIdValue identity)
-        putCacheNatural index
-    PreparedLeadingSetInductionFocus identity -> do
-        putCacheTag 0x01
-        putCacheNatural (Exact.exactLocalIdValue identity)
-
-putPreparedDischarge :: PreparedDischarge -> CachePut
-putPreparedDischarge
-        (PreparedVampireDischarge
-            _location justification goal _obligation) = do
-    putPreparedDischargeSyntax justification goal
-putPreparedDischarge
-        (PreparedSetExtensionality _location goal) = do
-    putCacheTag 0x03
-    putScopedProposition goal
-
-putPreparedDischargeSyntax
-    :: PreparedJustification
-    -> ScopedCheckedCore ObjectId
-    -> CachePut
-putPreparedDischargeSyntax justification goal = do
-    putPreparedJustification justification
-    putScopedProposition goal
-
-putPreparedCalculation :: PreparedCalculation -> CachePut
-putPreparedCalculation
-        (PreparedCheckedCalculation
-            operandType identities calculationGuard first links result) = do
-    putCoreTypeCache operandType
-    putCacheList
-        (putCacheNatural . Exact.exactLocalIdValue)
-        identities
-    putCacheMaybe putScopedProposition calculationGuard
-    putCacheList putScopedTerm
-        (first : (preparedCalculationLinkDestination <$> toList links))
-    putCacheList putPreparedDischarge
-        (preparedCalculationLinkDischarge <$> toList links)
-    putScopedProposition result
-
-putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut
-putPreparedSinceEvidence = \case
-    PreparedSinceExisting local -> do
-        putCacheTag 0x00
-        putPreparedLocalEvidence local
-    PreparedSinceDischarged discharge local -> do
-        putCacheTag 0x01
-        putPreparedDischarge discharge
-        putPreparedLocalEvidence local
-
-putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut
-putPreparedCaseAnalysis
-        (PreparedCaseAnalysis goal cases exhaustive discharge) = do
-    putScopedProposition goal
-    putCacheList putPreparedCase (toList cases)
-    putScopedProposition exhaustive
-    putPreparedDischarge discharge
-
-putPreparedCase :: PreparedCase -> CachePut
-putPreparedCase (PreparedCase assumption proof) = do
-    putScopedProposition assumption
-    putPreparedProof proof
-
-putPreparedLocalEvidence :: PreparedLocal -> CachePut
-putPreparedLocalEvidence
-        (PreparedLocal ordinal _origin support proposition) = do
-    putCacheNatural (Backend.localPremiseOrdinalValue ordinal)
-    putCacheList
-        (\(identity, coreType) -> do
-            putCacheNatural (Exact.exactLocalIdValue identity)
-            putCoreTypeCache coreType)
-        (Vector.toList support)
-    putScopedProposition proposition
-
-implicitAutoProofSyntaxId
-    :: ScopedCheckedCore ObjectId
-    -> ProofSyntaxId
-implicitAutoProofSyntaxId goal =
-    proofSyntaxId
-        (encodeCache do
-            putCacheTag 0x00
-            putPreparedDischargeSyntax PreparedAuto goal)
-
-putPreparedJustification :: PreparedJustification -> CachePut
-putPreparedJustification = \case
-    PreparedAuto ->
-        putCacheTag 0x00
-    PreparedReferences fingerprints -> do
-        putCacheTag 0x01
-        putCacheList
-            putSemanticFactOccurrenceFingerprintCache
-            (toList fingerprints)
-    PreparedLocalOnly ->
-        putCacheTag 0x02
-
-putScopedProposition
-    :: ScopedCheckedCore ObjectId
-    -> CachePut
-putScopedProposition proposition = do
-    putCacheList putCoreTypeCache
-        (scopedCoreContext proposition)
-    putCanonicalTermCache putObjectIdCache
-        (scopedCoreTerm proposition)
-
-putScopedTerm
-    :: ScopedCheckedCore ObjectId
-    -> CachePut
-putScopedTerm term = do
-    putCacheList putCoreTypeCache
-        (scopedCoreContext term)
-    putCoreTypeCache (scopedCoreType term)
-    putCanonicalTermCache putObjectIdCache
-        (scopedCoreTerm term)
-
-proofLocation :: Location -> Raw.Proof -> Location
-proofLocation fallback = \case
-    Raw.Omitted location -> location
-    Raw.Qed maybeLocation _justification ->
-        fromMaybe fallback maybeLocation
-    Raw.Contradiction location _justification -> location
-    Raw.ByCase location _cases -> location
-    Raw.ByContradiction location _proof -> location
-    Raw.BySetInduction location _term _proof -> location
-    Raw.ByOrdInduction location _proof -> location
-    Raw.Assume location _statement _proof -> location
-    Raw.FixSymbolic location _variables _bound _proof -> location
-    Raw.FixSuchThat location _variables _statement _proof -> location
-    Raw.Calc location _quantifier _calculation _proof -> location
-    Raw.TakeVar location _variables _bound _statement _justification _proof ->
-        location
-    Raw.TakeNoun location _noun _justification _proof -> location
-    Raw.Have location _since _statement _justification _proof -> location
-    Raw.Suffices location _statement _justification _proof -> location
-    Raw.Subclaim location _statement _subproof _proof -> location
-    Raw.Define location _variable _expression _proof -> location
-    Raw.DefineFunction location _function _argument _value _bound _domain _proof ->
-        location
-    Raw.DefineFunctionLocal
-            location _function _argument _value _bound _target _rules _proof ->
-        location
-
-throwProof :: ExactProofError -> Prepare value
-throwProof =
-    State.lift . Except.throwError
-
-liftDriver
-    :: Declaration.LoweringDriver value
-    -> Prepare value
-liftDriver =
-    State.lift . Except.lift
-
-stableUnique :: Ord value => [value] -> [value]
-stableUnique =
-    reverse . snd
-        . foldl'
-            (\(seen, reversed) value ->
-                if value `Set.member` seen
-                    then (seen, reversed)
-                    else
-                        ( Set.insert value seen
-                        , value : reversed
-                        ))
-            (Set.empty, [])