Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1443 deletions

diff --git a/source/Checking/Kernel/Proof.hs b/source/Checking/Kernel/Proof.hs
deleted file mode 100644
index 5fc0d96..0000000
--- a/source/Checking/Kernel/Proof.hs
+++ /dev/null
@@ -1,1443 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Small proof-producing natural-deduction combinators. Every resulting tree
--- is still replayed independently before it can authorize a fact.
-module Checking.Kernel.Proof
-    ( ProofContext
-    , rootProofContext
-    , proofContextTypes
-    , scopedTerm
-    , BuiltProof
-    , builtProofStatement
-    , builtProofDerivation
-    , importedProof
-    , foundationProof
-    , hypothesisProof
-    , implicationEliminationProof
-    , implicationIntroductionProof
-    , forallEliminationProof
-    , forallIntroductionProof
-    , falsumEliminationProof
-    , equalityReflexivityProof
-    , equalityReverseProof
-    , equalityCongruenceApplicationProof
-    , equalityModusPonensProof
-    , conversionProof
-    , doubleNegationEliminationProof
-    , conjunctionTerm
-    , conjunctionIntroductionProof
-    , conjunctionLeftProof
-    , conjunctionRightProof
-    , disjunctionTerm
-    , disjunctionLeftProof
-    , disjunctionRightProof
-    , disjunctionEliminationProof
-    , validateCaseAnalysisComposition
-    , validateDoubleNegationComposition
-    , validateFalsumEliminationComposition
-    , validateSetInductionComposition
-    , existentialTerm
-    , existentialIntroductionProof
-    , existentialEliminationProof
-    , setLfpBoundProof
-    , setLfpFixedProof
-    , setLfpInductProof
-    , KernelProofBuildError(..)
-    ) where
-
-import Base
-import Checking.Core
-import Checking.Foundation
-import Checking.Kernel.Derivation
-import Checking.Kernel.Semantics qualified as Semantics
-import Checking.Kernel.SetLfp qualified as SetLfp
-
-import Control.Monad (unless)
-import Data.Bifunctor (first)
-import Data.List qualified as List
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Text qualified as Text
-import Numeric.Natural (Natural)
-
-
-data ProofContext global = ProofContext
-    !CheckedFoundation
-    !(global -> Maybe CoreType)
-    ![CoreType]
-    ![ScopedCheckedCore global]
-
-rootProofContext
-    :: CheckedFoundation
-    -> (global -> Maybe CoreType)
-    -> ProofContext global
-rootProofContext foundation globalType =
-    ProofContext foundation globalType [] []
-
-proofContextTypes
-    :: ProofContext global
-    -> [CoreType]
-proofContextTypes
-        (ProofContext
-            _foundation
-            _globalType
-            context
-            _hypotheses) =
-    context
-
-data BuiltProof global = BuiltProof
-    !(ScopedCheckedCore global)
-    !(KernelDerivation global)
-
-builtProofStatement
-    :: BuiltProof global
-    -> ScopedCheckedCore global
-builtProofStatement
-        (BuiltProof statement _derivation) =
-    statement
-
-builtProofDerivation
-    :: BuiltProof global
-    -> KernelDerivation global
-builtProofDerivation
-        (BuiltProof _statement derivation) =
-    derivation
-
-data KernelProofBuildError
-    = ProofTermIllTyped !CoreCheckError
-    | ProofSemanticsFailed
-        !Semantics.KernelSemanticsError
-    | ProofFoundationArgumentMismatch
-        !FoundationAxiomTag
-    | ProofHypothesisNotFound
-    | ProofExpectedEquality
-    | ProofExpectedUnaryBinder
-    | ProofSetLfpRuleFailed !Text
-    | ProofConversionPlanFailed !Text
-    | ProofStructuralCompositionMismatch !Text
-    deriving stock (Show, Eq)
-
-scopedTerm
-    :: ProofContext global
-    -> CanonicalTerm global
-    -> Either
-        KernelProofBuildError
-        (ScopedCheckedCore global)
-scopedTerm
-        (ProofContext
-            _foundation
-            globalType
-            context
-            _hypotheses) =
-    first ProofTermIllTyped
-        . checkScopedCanonicalCore
-            globalType
-            context
-
-importedProof
-    :: ProofContext global
-    -> ImportIx
-    -> FrozenCheckedCore global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-importedProof context index statement =
-    pure
-        (BuiltProof
-            (embedClosedCore
-                (proofContextTypes context)
-                statement)
-            (importedFactDerivation index))
-
-foundationProof
-    :: ProofContext global
-    -> FoundationAxiomTag
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-foundationProof
-        context@(ProofContext
-            foundation
-            _globalType
-            _types
-            _hypotheses)
-        tag =
-    pure
-        (BuiltProof
-            (embedClosedCore
-                (proofContextTypes context)
-                (mapFrozenGlobals
-                    absurd
-                    (foundationAxiomFrozen
-                        foundation
-                        tag)))
-            (foundationFactDerivation tag))
-
-hypothesisProof
-    :: Eq global
-    => ProofContext global
-    -> ScopedCheckedCore global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-hypothesisProof
-        (ProofContext
-            _foundation
-            _globalType
-            _context
-            hypotheses)
-        statement =
-    case List.findIndex (== statement) hypotheses of
-        Nothing ->
-            Left ProofHypothesisNotFound
-        Just index ->
-            pure
-                (BuiltProof
-                    statement
-                    (localHypothesisDerivation
-                        (hypothesisIx
-                            (fromIntegral index))))
-
-implicationEliminationProof
-    :: Eq global
-    => ProofContext global
-    -> BuiltProof global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-implicationEliminationProof
-        (ProofContext
-            _foundation
-            globalType
-            _context
-            _hypotheses)
-        implication
-        premise = do
-    conclusion <-
-        first ProofSemanticsFailed
-            (Semantics.implicationElimination
-                globalType
-                (builtProofStatement implication)
-                (builtProofStatement premise))
-    pure
-        (BuiltProof
-            conclusion
-            (implicationEliminationDerivation
-                (builtProofDerivation implication)
-                (builtProofDerivation premise)))
-
-implicationIntroductionProof
-    :: ProofContext global
-    -> ScopedCheckedCore global
-    -> ( ProofContext global
-         -> BuiltProof global
-         -> Either
-            KernelProofBuildError
-            (BuiltProof global)
-       )
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-implicationIntroductionProof
-        (ProofContext
-            foundation
-            globalType
-            types
-            hypotheses)
-        premise
-        buildBody = do
-    let extended =
-            ProofContext
-                foundation
-                globalType
-                types
-                (premise : hypotheses)
-        premiseProof =
-            BuiltProof
-                premise
-                (localHypothesisDerivation
-                    (hypothesisIx 0))
-    body <-
-        buildBody extended premiseProof
-    conclusion <-
-        first ProofSemanticsFailed
-            (Semantics.implicationIntroduction
-                globalType
-                premise
-                (builtProofStatement body))
-    pure
-        (BuiltProof
-            conclusion
-            (implicationIntroductionDerivation
-                premise
-                (builtProofDerivation body)))
-
-forallEliminationProof
-    :: ProofContext global
-    -> BuiltProof global
-    -> ScopedCheckedCore global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-forallEliminationProof
-        (ProofContext
-            _foundation
-            globalType
-            _types
-            _hypotheses)
-        quantified
-        argument = do
-    conclusion <-
-        first ProofSemanticsFailed
-            (Semantics.forallElimination
-                globalType
-                (builtProofStatement quantified)
-                argument)
-    pure
-        (BuiltProof
-            conclusion
-            (forallEliminationDerivation
-                (builtProofDerivation quantified)
-                argument))
-
-forallIntroductionProof
-    :: ProofContext global
-    -> CoreType
-    -> ( ProofContext global
-         -> ScopedCheckedCore global
-         -> Either
-            KernelProofBuildError
-            (BuiltProof global)
-       )
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-forallIntroductionProof
-        (ProofContext
-            foundation
-            globalType
-            types
-            hypotheses)
-        binderType
-        buildBody = do
-    weakenedHypotheses <-
-        traverse
-            (first ProofTermIllTyped
-                . weakenScopedCore
-                    globalType
-                    binderType)
-            hypotheses
-    let extended =
-            ProofContext
-                foundation
-                globalType
-                (binderType : types)
-                weakenedHypotheses
-    variable <-
-        scopedTerm extended (CBound 0)
-    body <-
-        buildBody extended variable
-    conclusion <-
-        first ProofSemanticsFailed
-            (Semantics.forallIntroduction
-                globalType
-                binderType
-                (builtProofStatement body))
-    pure
-        (BuiltProof
-            conclusion
-            (forallIntroductionDerivation
-                binderType
-                (builtProofDerivation body)))
-
-falsumEliminationProof
-    :: ProofContext global
-    -> BuiltProof global
-    -> ScopedCheckedCore global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-falsumEliminationProof
-        (ProofContext
-            _foundation
-            globalType
-            _types
-            _hypotheses)
-        falsum
-        target = do
-    conclusion <-
-        first ProofSemanticsFailed
-            (Semantics.falsumElimination
-                globalType
-                (builtProofStatement falsum)
-                target)
-    pure
-        (BuiltProof
-            conclusion
-            (falsumEliminationDerivation
-                (builtProofDerivation falsum)
-                target))
-
-equalityReflexivityProof
-    :: ProofContext global
-    -> ScopedCheckedCore global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-equalityReflexivityProof
-        (ProofContext
-            _foundation
-            globalType
-            _types
-            _hypotheses)
-        operand = do
-    equality <-
-        first ProofSemanticsFailed
-            (Semantics.equalityReflexivity
-                globalType
-                operand)
-    pure
-        (BuiltProof
-            equality
-            (scopedEqualityReflexivityDerivation
-                operand))
-
-equalityCongruenceApplicationProof
-    :: ProofContext global
-    -> BuiltProof global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-equalityCongruenceApplicationProof
-        (ProofContext
-            _foundation
-            globalType
-            _types
-            _hypotheses)
-        functionEquality
-        argumentEquality = do
-    equality <-
-        first ProofSemanticsFailed
-            (Semantics.equalityCongruenceApplication
-                globalType
-                (builtProofStatement functionEquality)
-                (builtProofStatement argumentEquality))
-    pure
-        (BuiltProof
-            equality
-            (equalityCongruenceApplicationDerivation
-                (builtProofDerivation
-                    functionEquality)
-                (builtProofDerivation
-                    argumentEquality)))
-
-equalityModusPonensProof
-    :: Eq global
-    => ProofContext global
-    -> BuiltProof global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-equalityModusPonensProof
-        (ProofContext
-            _foundation
-            globalType
-            _types
-            _hypotheses)
-        equality
-        premise = do
-    conclusion <-
-        first ProofSemanticsFailed
-            (Semantics.equalityModusPonens
-                globalType
-                (builtProofStatement equality)
-                (builtProofStatement premise))
-    pure
-        (BuiltProof
-            conclusion
-            (equalityModusPonensDerivation
-                (builtProofDerivation equality)
-                (builtProofDerivation premise)))
-
-conversionProof
-    :: Eq global
-    => ProofContext global
-    -> BuiltProof global
-    -> ScopedCheckedCore global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-conversionProof
-        (ProofContext
-            _foundation
-            globalType
-            _types
-            _hypotheses)
-        source
-        target = do
-    plan <-
-        first (ProofConversionPlanFailed . Text.pack . show)
-            (conversionPlan 100000)
-    result <-
-        first ProofSemanticsFailed
-            (Semantics.convertJudgment
-                globalType
-                (conversionPlanBudget plan)
-                (builtProofStatement source)
-                target)
-    pure
-        (BuiltProof
-            result
-            (convertJudgmentDerivation
-                (builtProofDerivation source)
-                target
-                plan))
-
-equalityReverseProof
-    :: Eq global
-    => ProofContext global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-equalityReverseProof context equality = do
-    (operandType, left, right) <-
-        equalityParts
-            (builtProofStatement equality)
-    leftOperand <-
-        scopedTerm context left
-    weakenedLeft <-
-        first ProofTermIllTyped
-            (weakenScopedCore
-                (contextGlobalType context)
-                operandType
-                leftOperand)
-    function <-
-        scopedTerm context
-            (CLam operandType
-                (CEq
-                    operandType
-                    (CBound 0)
-                    (scopedCoreTerm
-                        weakenedLeft)))
-    functionReflexivity <-
-        equalityReflexivityProof
-            context
-            function
-    appliedEquality <-
-        equalityCongruenceApplicationProof
-            context
-            functionReflexivity
-            equality
-    leftReflexivity <-
-        equalityReflexivityProof
-            context
-            leftOperand
-    appliedLeft <-
-        scopedTerm context
-            (CApp
-                (scopedCoreTerm function)
-                left)
-    appliedLeftReflexivity <-
-        conversionProof
-            context
-            leftReflexivity
-            appliedLeft
-    reversedApplication <-
-        equalityModusPonensProof
-            context
-            appliedEquality
-            appliedLeftReflexivity
-    expected <-
-        scopedTerm context
-            (CEq operandType right left)
-    conversionProof
-        context
-        reversedApplication
-        expected
-
-doubleNegationEliminationProof
-    :: Eq global
-    => ProofContext global
-    -> ScopedCheckedCore global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-doubleNegationEliminationProof
-        context
-        target
-        doubleNegation = do
-    axiom <-
-        foundationProof
-            context
-            DoubleNegationElim
-    instanceProof <-
-        forallEliminationProof
-            context
-            axiom
-            target
-    implicationEliminationProof
-        context
-        instanceProof
-        doubleNegation
-
-conjunctionTerm
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-conjunctionTerm left right =
-    CImp
-        (CImp left
-            (CImp right CFalsum))
-        CFalsum
-
-conjunctionIntroductionProof
-    :: Eq global
-    => ProofContext global
-    -> BuiltProof global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-conjunctionIntroductionProof
-        context
-        left
-        right = do
-    let leftTerm =
-            scopedCoreTerm
-                (builtProofStatement left)
-        rightTerm =
-            scopedCoreTerm
-                (builtProofStatement right)
-    refuter <-
-        scopedTerm context
-            (CImp leftTerm
-                (CImp rightTerm CFalsum))
-    implicationIntroductionProof
-        context
-        refuter
-        (\extended refuterProof -> do
-            firstApplication <-
-                implicationEliminationProof
-                    extended
-                    refuterProof
-                    (weakenForHypothesis left)
-            implicationEliminationProof
-                extended
-                firstApplication
-                (weakenForHypothesis right))
-
-conjunctionLeftProof
-    :: Eq global
-    => ProofContext global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-conjunctionLeftProof context left right conjunction = do
-    leftProposition <-
-        scopedTerm context left
-    notLeft <-
-        scopedTerm context
-            (CImp left CFalsum)
-    doubleNegation <-
-        implicationIntroductionProof
-            context
-            notLeft
-            (\withNotLeft _notLeftProof -> do
-                leftAtRefuter <-
-                    scopedTerm withNotLeft left
-                refuterProof <-
-                    implicationIntroductionProof
-                        withNotLeft
-                        leftAtRefuter
-                        (\withLeft leftProof -> do
-                            rightProposition <-
-                                scopedTerm withLeft right
-                            implicationIntroductionProof
-                                withLeft
-                                rightProposition
-                                (\withBoth _rightProof -> do
-                                    notLeftCurrent <-
-                                        hypothesisProof
-                                            withBoth
-                                            notLeft
-                                    implicationEliminationProof
-                                        withBoth
-                                        notLeftCurrent
-                                        (weakenForHypothesis
-                                            leftProof)))
-                implicationEliminationProof
-                    withNotLeft
-                    (weakenForHypothesis conjunction)
-                    refuterProof)
-    doubleNegationEliminationProof
-        context
-        leftProposition
-        doubleNegation
-
-conjunctionRightProof
-    :: Eq global
-    => ProofContext global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-conjunctionRightProof context left right conjunction = do
-    rightProposition <-
-        scopedTerm context right
-    notRight <-
-        scopedTerm context
-            (CImp right CFalsum)
-    doubleNegation <-
-        implicationIntroductionProof
-            context
-            notRight
-            (\withNotRight _notRightProof -> do
-                leftAtRefuter <-
-                    scopedTerm withNotRight left
-                refuterProof <-
-                    implicationIntroductionProof
-                        withNotRight
-                        leftAtRefuter
-                        (\withLeft _leftProof -> do
-                            rightAtLeft <-
-                                scopedTerm
-                                    withLeft
-                                    right
-                            implicationIntroductionProof
-                                withLeft
-                                rightAtLeft
-                                (\withBoth rightProof -> do
-                                    notRightCurrent <-
-                                        hypothesisProof
-                                            withBoth
-                                            notRight
-                                    implicationEliminationProof
-                                        withBoth
-                                        notRightCurrent
-                                        rightProof))
-                implicationEliminationProof
-                    withNotRight
-                    (weakenForHypothesis conjunction)
-                    refuterProof)
-    doubleNegationEliminationProof
-        context
-        rightProposition
-        doubleNegation
-
-disjunctionTerm
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-disjunctionTerm left right =
-    CImp
-        (CImp left CFalsum)
-        right
-
-disjunctionLeftProof
-    :: Eq global
-    => ProofContext global
-    -> CanonicalTerm global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-disjunctionLeftProof context right leftProof = do
-    notLeft <-
-        scopedTerm context
-            (CImp
-                (scopedCoreTerm
-                    (builtProofStatement leftProof))
-                CFalsum)
-    rightTarget <-
-        scopedTerm context right
-    implicationIntroductionProof
-        context
-        notLeft
-        (\extended notLeftProof -> do
-            falsum <-
-                implicationEliminationProof
-                    extended
-                    notLeftProof
-                    (weakenForHypothesis
-                        leftProof)
-            falsumEliminationProof
-                extended
-                falsum
-                rightTarget)
-
-disjunctionRightProof
-    :: ProofContext global
-    -> CanonicalTerm global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-disjunctionRightProof context left rightProof = do
-    notLeft <-
-        scopedTerm context
-            (CImp left CFalsum)
-    implicationIntroductionProof
-        context
-        notLeft
-        (\_extended _notLeftProof ->
-            pure
-                (weakenForHypothesis
-                    rightProof))
-
-disjunctionEliminationProof
-    :: Eq global
-    => ProofContext global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-    -> BuiltProof global
-    -> ScopedCheckedCore global
-    -> ( ProofContext global
-         -> BuiltProof global
-         -> Either
-            KernelProofBuildError
-            (BuiltProof global)
-       )
-    -> ( ProofContext global
-         -> BuiltProof global
-         -> Either
-            KernelProofBuildError
-            (BuiltProof global)
-       )
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-disjunctionEliminationProof
-        context
-        left
-        right
-        disjunction
-        result
-        leftCase
-        rightCase = do
-    leftProposition <-
-        scopedTerm context left
-    rightProposition <-
-        scopedTerm context right
-    leftImplication <-
-        implicationIntroductionProof
-            context
-            leftProposition
-            leftCase
-    rightImplication <-
-        implicationIntroductionProof
-            context
-            rightProposition
-            rightCase
-    notResult <-
-        scopedTerm context
-            (CImp
-                (scopedCoreTerm result)
-                CFalsum)
-    doubleNegation <-
-        implicationIntroductionProof
-            context
-            notResult
-            (\extended notResultProof -> do
-                leftAtNotResult <-
-                    scopedTerm extended left
-                notLeftProof <-
-                    implicationIntroductionProof
-                        extended
-                        leftAtNotResult
-                        (\withLeft leftProof -> do
-                            resultProof <-
-                                implicationEliminationProof
-                                    withLeft
-                                    (weakenForHypothesis
-                                        (weakenForHypothesis
-                                            leftImplication))
-                                    leftProof
-                            implicationEliminationProof
-                                withLeft
-                                (weakenForHypothesis
-                                    notResultProof)
-                                resultProof)
-                rightProof <-
-                    implicationEliminationProof
-                        extended
-                        (weakenForHypothesis
-                            disjunction)
-                        notLeftProof
-                resultProof <-
-                    implicationEliminationProof
-                        extended
-                        (weakenForHypothesis
-                            rightImplication)
-                        rightProof
-                implicationEliminationProof
-                    extended
-                    notResultProof
-                    resultProof)
-    doubleNegationEliminationProof
-        context
-        result
-        doubleNegation
-
--- | Validate the one structural rule used by exact source case analysis.
--- The branch proofs and the exhaustive disjunction are represented here by
--- exact hypotheses; the kernel combinators must derive the owned goal from
--- precisely those propositions.  No derived proof escapes this check.
-validateCaseAnalysisComposition
-    :: Eq global
-    => CheckedFoundation
-    -> (global -> Maybe CoreType)
-    -> ScopedCheckedCore global
-    -> NonEmpty (ScopedCheckedCore global)
-    -> ScopedCheckedCore global
-    -> Either KernelProofBuildError ()
-validateCaseAnalysisComposition
-        foundation globalType goal cases exhaustive = do
-    validatePropositionContext "case goal" lexicalContext goal
-    traverse_
-        (validatePropositionContext "case assumption" lexicalContext)
-        cases
-    validatePropositionContext
-        "case exhaustiveness target" lexicalContext exhaustive
-    let expectedExhaustive =
-            foldl1
-                (\left right ->
-                    CImp
-                        (CImp left CFalsum)
-                        right)
-                (scopedCoreTerm <$> cases)
-    unless (scopedCoreTerm exhaustive == expectedExhaustive)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "case exhaustiveness is not the source-ordered disjunction"))
-    branchImplications <-
-        traverse
-            (checkedImplication lexicalContext goal)
-            cases
-    let context =
-            ProofContext
-                foundation
-                globalType
-                lexicalContext
-                (exhaustive : toList branchImplications)
-    exhaustiveProof <- hypothesisProof context exhaustive
-    result <-
-        eliminateCases
-            context goal cases exhaustiveProof
-    unless (builtProofStatement result == goal)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "case elimination did not derive the owned goal"))
-  where
-    lexicalContext = scopedCoreContext goal
-
-    checkedImplication expectedContext conclusion antecedent =
-        case implyScopedCore antecedent conclusion of
-            Just implication
-                | scopedCoreContext implication == expectedContext ->
-                    pure implication
-            _ ->
-                Left
-                    (ProofStructuralCompositionMismatch
-                        "case branch implication changed context")
-
-    eliminateCases context result (only :| []) caseProof = do
-        branchImplication <-
-            scopedTerm context
-                (CImp
-                    (scopedCoreTerm only)
-                    (scopedCoreTerm result))
-            >>= hypothesisProof context
-        implicationEliminationProof context branchImplication caseProof
-    eliminateCases context result (firstCase :| rest) disjunctionProof = do
-        let allCases = firstCase :| rest
-            leftCases = NonEmpty.fromList (NonEmpty.init allCases)
-            rightCase = NonEmpty.last allCases
-            leftTerm =
-                foldl1 disjunctionTerm
-                    (scopedCoreTerm <$> leftCases)
-        disjunctionEliminationProof
-            context
-            leftTerm
-            (scopedCoreTerm rightCase)
-            disjunctionProof
-            result
-            (\extended leftProof ->
-                eliminateCases extended result leftCases leftProof)
-            (\extended rightProof -> do
-                branchImplication <-
-                    scopedTerm extended
-                        (CImp
-                            (scopedCoreTerm rightCase)
-                            (scopedCoreTerm result))
-                        >>= hypothesisProof extended
-                implicationEliminationProof
-                    extended branchImplication rightProof)
-
--- | Validate the exact classical closing step for a proof by contradiction.
--- The only classical input is the confined 'DoubleNegationElim' foundation
--- row already consumed by 'doubleNegationEliminationProof'.
-validateDoubleNegationComposition
-    :: Eq global
-    => CheckedFoundation
-    -> (global -> Maybe CoreType)
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> Either KernelProofBuildError ()
-validateDoubleNegationComposition
-        foundation globalType goal negation falsum = do
-    let lexicalContext = scopedCoreContext goal
-    validatePropositionContext "contradiction goal" lexicalContext goal
-    validatePropositionContext
-        "contradiction negation" lexicalContext negation
-    validatePropositionContext "contradiction falsum" lexicalContext falsum
-    unless (scopedCoreTerm falsum == CFalsum)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "proof by contradiction did not target falsum"))
-    expectedNegation <-
-        checkedNegation lexicalContext goal
-    unless (negation == expectedNegation)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "proof by contradiction did not own the exact negated goal"))
-    doubleNegation <-
-        checkedNegation lexicalContext negation
-    let context =
-            ProofContext
-                foundation globalType lexicalContext [doubleNegation]
-    hypothesis <- hypothesisProof context doubleNegation
-    result <- doubleNegationEliminationProof context goal hypothesis
-    unless (builtProofStatement result == goal)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "double-negation elimination did not derive the owned goal"))
-
--- | Validate the exact ex-falso closing step used after a terminal indirect
--- contradiction discharge.
-validateFalsumEliminationComposition
-    :: Eq global
-    => CheckedFoundation
-    -> (global -> Maybe CoreType)
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> Either KernelProofBuildError ()
-validateFalsumEliminationComposition foundation globalType goal falsum = do
-    let lexicalContext = scopedCoreContext goal
-    validatePropositionContext "contradiction goal" lexicalContext goal
-    validatePropositionContext "contradiction falsum" lexicalContext falsum
-    unless (scopedCoreTerm falsum == CFalsum)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "falsum elimination did not receive falsum"))
-    let context =
-            ProofContext foundation globalType lexicalContext [falsum]
-    hypothesis <- hypothesisProof context falsum
-    result <- falsumEliminationProof context hypothesis goal
-    unless (builtProofStatement result == goal)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "falsum elimination did not derive the owned goal"))
-
--- | Validate the exact structural instance used by source set induction.
--- The admitted child is represented by its generalized step proposition;
--- the checked foundation row must specialize to that exact premise and the
--- owned binder-level result. No induction principle becomes an ATP premise.
-validateSetInductionComposition
-    :: Eq global
-    => CheckedFoundation
-    -> (global -> Maybe CoreType)
-    -> Natural
-    -> ScopedCheckedCore global
-    -> [ScopedCheckedCore global]
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> Either KernelProofBuildError ()
-validateSetInductionComposition
-        foundation globalType selected property antecedents childTarget
-        hypothesis result = do
-    let lexicalContext = scopedCoreContext property
-    traverse_
-        (validatePropositionContext
-            "set-induction antecedent" lexicalContext)
-        antecedents
-    validatePropositionContext
-        "set-induction property" lexicalContext property
-    validatePropositionContext
-        "set-induction child target" lexicalContext childTarget
-    validatePropositionContext
-        "set-induction hypothesis" lexicalContext hypothesis
-    validatePropositionContext
-        "set-induction result" lexicalContext result
-    expectedProperty <-
-        foldrM implyChecked childTarget antecedents
-    unless (property == expectedProperty)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "set-induction property does not own the child target and guards"))
-    (predicate, expectedHypothesis, step, expectedResult) <-
-        maybe
-            (Left
-                (ProofStructuralCompositionMismatch
-                    "set-induction focus is not a set-valued ambient binder"))
-            pure
-            (scopedSetInductionInstance selected property)
-    unless (hypothesis == expectedHypothesis)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "set-induction hypothesis does not match the owned property"))
-    unless (result == expectedResult)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "set-induction result does not close the owned property"))
-    let context =
-            ProofContext foundation globalType lexicalContext [step]
-    stepProof <- hypothesisProof context step
-    axiom <- foundationProof context SetInduction
-    instanceProof <- forallEliminationProof context axiom predicate
-    expectedInstance <-
-        maybe
-            (Left
-                (ProofStructuralCompositionMismatch
-                    "set-induction instance changed lexical context"))
-            pure
-            (implyScopedCore step result)
-    convertedInstance <-
-        conversionProof context instanceProof expectedInstance
-    resultProof <-
-        implicationEliminationProof context convertedInstance stepProof
-    unless (builtProofStatement resultProof == result)
-        (Left
-            (ProofStructuralCompositionMismatch
-                "set-induction foundation instance did not derive the owned result"))
-  where
-    implyChecked antecedent conclusion =
-        maybe
-            (Left
-                (ProofStructuralCompositionMismatch
-                    "set-induction guard changed lexical context"))
-            pure
-            (implyScopedCore antecedent conclusion)
-
-validatePropositionContext
-    :: Text
-    -> [CoreType]
-    -> ScopedCheckedCore global
-    -> Either KernelProofBuildError ()
-validatePropositionContext label expected proposition =
-    unless
-        ( scopedCoreType proposition == TyProp
-            && scopedCoreContext proposition == expected
-        )
-        (Left
-            (ProofStructuralCompositionMismatch
-                (label <> " has the wrong type or lexical context")))
-
-checkedNegation
-    :: [CoreType]
-    -> ScopedCheckedCore global
-    -> Either KernelProofBuildError (ScopedCheckedCore global)
-checkedNegation expectedContext proposition =
-    case negateScopedCore proposition of
-        Just negation
-            | scopedCoreContext negation == expectedContext ->
-                pure negation
-        _ ->
-            Left
-                (ProofStructuralCompositionMismatch
-                    "classical negation changed context")
-
-existentialTerm
-    :: CoreType
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-existentialTerm binderType body =
-    CImp
-        (CForall binderType
-            (CImp body CFalsum))
-        CFalsum
-
-existentialIntroductionProof
-    :: Eq global
-    => ProofContext global
-    -> CoreType
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-existentialIntroductionProof
-        context
-        binderType
-        bodyUnderBinder
-        witness
-        bodyAtWitness = do
-    unless
-        (proofContextTypes context
-            == drop 1
-                (scopedCoreContext
-                    bodyUnderBinder))
-        (Left ProofExpectedUnaryBinder)
-    universalNegation <-
-        scopedTerm context
-            (CForall binderType
-                (CImp
-                    (scopedCoreTerm
-                        bodyUnderBinder)
-                    CFalsum))
-    implicationIntroductionProof
-        context
-        universalNegation
-        (\extended universalProof -> do
-            negatedBody <-
-                forallEliminationProof
-                    extended
-                    universalProof
-                    witness
-            implicationEliminationProof
-                extended
-                negatedBody
-                (weakenForHypothesis
-                    bodyAtWitness))
-
-existentialEliminationProof
-    :: Eq global
-    => ProofContext global
-    -> CoreType
-    -> ScopedCheckedCore global
-    -> BuiltProof global
-    -> ScopedCheckedCore global
-    -> ( ProofContext global
-         -> ScopedCheckedCore global
-         -> BuiltProof global
-         -> Either
-            KernelProofBuildError
-            (BuiltProof global)
-       )
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-existentialEliminationProof
-        context
-        binderType
-        bodyUnderBinder
-        existential
-        result
-        bodyCase = do
-    notResult <-
-        scopedTerm context
-            (CImp
-                (scopedCoreTerm result)
-                CFalsum)
-    notResultUnderBinder <-
-        first ProofTermIllTyped
-            (weakenScopedCore
-                (contextGlobalType context)
-                binderType
-                notResult)
-    doubleNegation <-
-        implicationIntroductionProof
-            context
-            notResult
-            (\withNotResult _notResultProof -> do
-                universalNegation <-
-                    forallIntroductionProof
-                        withNotResult
-                        binderType
-                        (\withBinder variable -> do
-                            let body =
-                                    bodyUnderBinder
-                            implicationIntroductionProof
-                                withBinder
-                                body
-                                (\withBody bodyProof -> do
-                                    resultProof <-
-                                        bodyCase
-                                            withBody
-                                            variable
-                                            bodyProof
-                                    notResultCurrent <-
-                                        hypothesisProof
-                                            withBody
-                                            notResultUnderBinder
-                                    implicationEliminationProof
-                                        withBody
-                                        notResultCurrent
-                                        resultProof))
-                implicationEliminationProof
-                    withNotResult
-                    (weakenForHypothesis
-                        existential)
-                    universalNegation)
-    doubleNegationEliminationProof
-        context
-        result
-        doubleNegation
-
-setLfpBoundProof
-    :: ProofContext global
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-setLfpBoundProof
-        (ProofContext
-            foundation
-            globalType
-            _types
-            _hypotheses)
-        domain
-        operator = do
-    result <-
-        first (ProofSetLfpRuleFailed . Text.pack . show)
-            (SetLfp.setLfpBound
-                foundation
-                globalType
-                domain
-                operator)
-    pure
-        (BuiltProof
-            result
-            (setLfpBoundDerivation
-                domain
-                operator))
-
-setLfpFixedProof
-    :: Eq global
-    => ProofContext global
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-setLfpFixedProof
-        (ProofContext
-            foundation
-            globalType
-            _types
-            _hypotheses)
-        domain
-        operator
-        monotone = do
-    result <-
-        first (ProofSetLfpRuleFailed . Text.pack . show)
-            (SetLfp.setLfpFixed
-                foundation
-                globalType
-                domain
-                operator
-                (builtProofStatement
-                    monotone))
-    pure
-        (BuiltProof
-            result
-            (setLfpFixedDerivation
-                domain
-                operator
-                (builtProofDerivation
-                    monotone)))
-
-setLfpInductProof
-    :: Eq global
-    => ProofContext global
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> BuiltProof global
-    -> BuiltProof global
-    -> BuiltProof global
-    -> Either
-        KernelProofBuildError
-        (BuiltProof global)
-setLfpInductProof
-        (ProofContext
-            foundation
-            globalType
-            _types
-            _hypotheses)
-        domain
-        operator
-        predicate
-        element
-        monotone
-        member
-        closure = do
-    result <-
-        first (ProofSetLfpRuleFailed . Text.pack . show)
-            (SetLfp.setLfpInduct
-                foundation
-                globalType
-                domain
-                operator
-                predicate
-                element
-                (builtProofStatement
-                    monotone)
-                (builtProofStatement
-                    member)
-                (builtProofStatement
-                    closure))
-    pure
-        (BuiltProof
-            result
-            (setLfpInductDerivation
-                domain
-                operator
-                predicate
-                element
-                (builtProofDerivation
-                    monotone)
-                (builtProofDerivation
-                    member)
-                (builtProofDerivation
-                    closure)))
-
-contextGlobalType
-    :: ProofContext global
-    -> (global -> Maybe CoreType)
-contextGlobalType
-        (ProofContext
-            _foundation
-            globalType
-            _types
-            _hypotheses) =
-    globalType
-
-equalityParts
-    :: ScopedCheckedCore global
-    -> Either
-        KernelProofBuildError
-        ( CoreType
-        , CanonicalTerm global
-        , CanonicalTerm global
-        )
-equalityParts equality =
-    case scopedCoreTerm equality of
-        CEq operandType left right ->
-            Right (operandType, left, right)
-        _ ->
-            Left ProofExpectedEquality
-
-weakenForHypothesis
-    :: BuiltProof global
-    -> BuiltProof global
-weakenForHypothesis
-        (BuiltProof statement derivation) =
-    BuiltProof
-        statement
-        (weakenDerivationHypotheses 1 derivation)