# eukhe: the proofs. Each law of laws/<area>.bend is proven in
# proof/<area>/<law>.bend from the lemmas of its area (proof/<area>/base.bend)
# and of every area (proof/base.bend). `bend PROOF.bend --verdict` checks them all.

import Base
import ./LAWS.bend as Laws
import ./proof/base/bool.bend as LBool
import ./proof/base/child.bend as LChild
import ./proof/base/command.bend as LCommand
import ./proof/base/director.bend as LDirector
import ./proof/base/effort.bend as LEffort
import ./proof/base/fsmode.bend as LFsmode
import ./proof/base/list.bend as LList
import ./proof/base/logic/bool.bend as LLogicBool
import ./proof/base/logic/list.bend as LLogicList
import ./proof/base/logic/logic.bend as LLogicLogic
import ./proof/base/logic/maybe.bend as LLogicMaybe
import ./proof/base/logic/nat.bend as LLogicNat
import ./proof/base/logic/semver.bend as LLogicSemver
import ./proof/base/logic/string.bend as LLogicString
import ./proof/base/logic/wire.bend as LLogicWire
import ./proof/base/nat.bend as LNat
import ./proof/base/optchat.bend as LOptchat
import ./proof/base/pair.bend as LPair
import ./proof/base/progress.bend as LProgress
import ./proof/base/replace.bend as LReplace
import ./proof/base/retry.bend as LRetry
import ./proof/base/run.bend as LRun
import ./proof/base/semver.bend as LSemver
import ./proof/base/string.bend as LString
import ./proof/base/tree.bend as LTree
import ./proof/base/wire.bend as LWire
import ./proof/base/wire_dec.bend as LWireDec
import ./proof/base/wire_strs.bend as LWireStrs
import ./proof/optchat/base.bend as LAOptchat
import ./proof/optchat/view_covers.bend as PViewCovers
import ./proof/optchat/cview_covers.bend as PCviewCovers
import ./proof/optchat/message_appends.bend as PMessageAppends
import ./proof/optchat/message_merges_nothing.bend as PMessageMergesNothing
import ./proof/optchat/merge_is_one_pair.bend as PMergeIsOnePair
import ./proof/optchat/merge_covers.bend as PMergeCovers
import ./proof/optchat/push_agrees.bend as PPushAgrees
import ./proof/optchat/push_agrees_always.bend as PPushAgreesAlways
import ./proof/optchat/push_agrees_always/list.bend as LLPushAgreesAlwaysList
import ./proof/optchat/push_agrees_always/logic.bend as LLPushAgreesAlwaysLogic
import ./proof/optchat/push_agrees_always/nat.bend as LLPushAgreesAlwaysNat
import ./proof/optchat/push_agrees_always/optchat.bend as LLPushAgreesAlwaysOptchat
import ./proof/optchat/push_agrees_always/pair.bend as LLPushAgreesAlwaysPair
import ./proof/optchat/fit_reaches_budget.bend as PFitReachesBudget
import ./proof/optchat/fit_merges_built.bend as PFitMergesBuilt
import ./proof/optchat/view_summarized.bend as PViewSummarized
import ./proof/optchat/cview_summarized.bend as PCviewSummarized
import ./proof/optchat/last_merges_8_9.bend as PLastMerges89
import ./proof/optchat/first_merges_0_7.bend as PFirstMerges07
import ./proof/optchat/first_is_not_last.bend as PFirstIsNotLast
import ./proof/optchat/first_leaves_push.bend as PFirstLeavesPush
import ./proof/optchat/context_ends_at_node.bend as PContextEndsAtNode
import ./proof/optchat/context_is_prefix.bend as PContextIsPrefix
import ./proof/optchat/need_progress.bend as PNeedProgress
import ./proof/compactor/base.bend as LACompactor
import ./proof/compactor/line_calls_at_most_tries.bend as PLineCallsAtMostTries
import ./proof/compactor/line_fits.bend as PLineFits
import ./proof/compactor/line_takes_first_fit.bend as PLineTakesFirstFit
import ./proof/compactor/line_stops_when_not_shorter.bend as PLineStopsWhenNotShorter
import ./proof/compactor/line_empty_is_a_try.bend as PLineEmptyIsATry
import ./proof/compactor/line_error_fails.bend as PLineErrorFails
import ./proof/compactor/fail_cap_builds.bend as PFailCapBuilds
import ./proof/compactor/need_first.bend as PNeedFirst
import ./proof/compactor/need_first_running.bend as PNeedFirstRunning
import ./proof/compactor/wait_keeps_needed.bend as PWaitKeepsNeeded
import ./proof/compactor/settle_falls.bend as PSettleFalls
import ./proof/compactor/settle_bounded.bend as PSettleBounded
import ./proof/compactor/settle_reached.bend as PSettleReached
import ./proof/compactor/settle_start.bend as PSettleStart
import ./proof/compactor/line_open_exact.bend as PLineOpenExact
import ./proof/compactor/line_step_exact.bend as PLineStepExact
import ./proof/compactor/pend_after_exact.bend as PPendAfterExact
import ./proof/compactor/line_fits_exact.bend as PLineFitsExact
import ./proof/compactor/line_first_exact.bend as PLineFirstExact
import ./proof/compactor/first_fit_exact.bend as PFirstFitExact
import ./proof/compactor/read_exact.bend as PReadExact
import ./proof/compactor/failures_exact.bend as PFailuresExact
import ./proof/compactor/pend_pending_exact.bend as PPendPendingExact
import ./proof/compactor/line_steps.bend as PLineSteps
import ./proof/compactor/compactor_ffi_open.bend as PCompactorFfiOpen
import ./proof/compactor/compactor_ffi_step.bend as PCompactorFfiStep
import ./proof/compactor/compactor_ffi_after.bend as PCompactorFfiAfter
import ./proof/compactor/compactor_ffi_malformed_exact.bend as PCompactorFfiMalformedExact
import ./proof/compactor/compactor_ffi_example.bend as PCompactorFfiExample
import ./proof/wait/base.bend as LAWait
import ./proof/wait/wait_ends_once.bend as PWaitEndsOnce
import ./proof/wait/wait_end_is_final.bend as PWaitEndIsFinal
import ./proof/wait/wait_arrival_wins.bend as PWaitArrivalWins
import ./proof/wait/wait_cancel_wins.bend as PWaitCancelWins
import ./proof/lease/base.bend as LALease
import ./proof/lease/lease_fifo.bend as PLeaseFifo
import ./proof/lease/lease_never_idle.bend as PLeaseNeverIdle
import ./proof/lease/lease_keeps_waiters.bend as PLeaseKeepsWaiters
import ./proof/lease/lease_stop_never_holds.bend as PLeaseStopNeverHolds
import ./proof/lease/lease_crash_frees.bend as PLeaseCrashFrees
import ./proof/child/base.bend as LAChild
import ./proof/child/child_stalls_in_time.bend as PChildStallsInTime
import ./proof/child/child_unreachable_in_time.bend as PChildUnreachableInTime
import ./proof/child/child_clock_bounded.bend as PChildClockBounded
import ./proof/child/child_progress_is_not_a_stall.bend as PChildProgressIsNotAStall
import ./proof/child/child_one_live.bend as PChildOneLive
import ./proof/child/child_report_once.bend as PChildReportOnce
import ./proof/child/child_resubmits_per_abort.bend as PChildResubmitsPerAbort
import ./proof/child/child_delivered_once.bend as PChildDeliveredOnce
import ./proof/child/child_task_call.bend as PChildTaskCall
import ./proof/child/child_silent_never_reports.bend as PChildSilentNeverReports
import ./proof/child/child_report_move.bend as PChildReportMove
import ./proof/child/child_report_move_is_owe.bend as PChildReportMoveIsOwe
import ./proof/child/child_abort_rule.bend as PChildAbortRule
import ./proof/child/child_entry_verdict.bend as PChildEntryVerdict
import ./proof/child/child_entry_move.bend as PChildEntryMove
import ./proof/child/child_entry_abort.bend as PChildEntryAbort
import ./proof/admission/base/admission/St.bend as LAAdmissionAdmissionSt
import ./proof/admission/base/admission/bit.bend as LAAdmissionAdmissionBit
import ./proof/admission/base/admission/calm.bend as LAAdmissionAdmissionCalm
import ./proof/admission/base/admission/cnt.bend as LAAdmissionAdmissionCnt
import ./proof/admission/base/admission/collect.bend as LAAdmissionAdmissionCollect
import ./proof/admission/base/admission/ended.bend as LAAdmissionAdmissionEnded
import ./proof/admission/base/admission/get.bend as LAAdmissionAdmissionGet
import ./proof/admission/base/admission/hit.bend as LAAdmissionAdmissionHit
import ./proof/admission/base/admission/isz.bend as LAAdmissionAdmissionIsz
import ./proof/admission/base/admission/le.bend as LAAdmissionAdmissionLe
import ./proof/admission/base/admission/lv.bend as LAAdmissionAdmissionLv
import ./proof/admission/base/admission/pick.bend as LAAdmissionAdmissionPick
import ./proof/admission/base/admission/pot.bend as LAAdmissionAdmissionPot
import ./proof/admission/base/admission/release.bend as LAAdmissionAdmissionRelease
import ./proof/admission/base/admission/room.bend as LAAdmissionAdmissionRoom
import ./proof/admission/base/admission/step.bend as LAAdmissionAdmissionStep
import ./proof/admission/base/admission/waits.bend as LAAdmissionAdmissionWaits
import ./proof/admission/base/bool.bend as LAAdmissionBool
import ./proof/admission/base/list.bend as LAAdmissionList
import ./proof/admission/base/logic.bend as LAAdmissionLogic
import ./proof/admission/base/nat.bend as LAAdmissionNat
import ./proof/admission/base/wire.bend as LAAdmissionWire
import ./proof/admission/admission_preempts.bend as PAdmissionPreempts
import ./proof/admission/admission_capacity.bend as PAdmissionCapacity
import ./proof/admission/admission_no_lost_wakeup.bend as PAdmissionNoLostWakeup
import ./proof/admission/admission_background_yields.bend as PAdmissionBackgroundYields
import ./proof/admission/admission_fifo.bend as PAdmissionFifo
import ./proof/admission/admission_interactive_step.bend as PAdmissionInteractiveStep
import ./proof/admission/admission_interactive_bound.bend as PAdmissionInteractiveBound
import ./proof/admission/admission_ended_stays_ended.bend as PAdmissionEndedStaysEnded
import ./proof/admission/admission_end_twice_changes_nothing.bend as PAdmissionEndTwiceChangesNothing
import ./proof/admission/admission_every_ticket_ends.bend as PAdmissionEveryTicketEnds
import ./proof/admission/admission_live_step.bend as PAdmissionLiveStep
import ./proof/admission/admission_live_run.bend as PAdmissionLiveRun
import ./proof/admission/admission_live_example.bend as PAdmissionLiveExample
import ./proof/admission/adw_cls_round_trip.bend as PAdwClsRoundTrip
import ./proof/admission/adw_sts_round_trip.bend as PAdwStsRoundTrip
import ./proof/admission/adw_lv_round_trip.bend as PAdwLvRoundTrip
import ./proof/admission/adw_lvs_round_trip.bend as PAdwLvsRoundTrip
import ./proof/admission/adw_live_round_trip.bend as PAdwLiveRoundTrip
import ./proof/admission/adw_open_answers.bend as PAdwOpenAnswers
import ./proof/admission/adw_step_answers.bend as PAdwStepAnswers
import ./proof/admission/adw_open_malformed.bend as PAdwOpenMalformed
import ./proof/admission/adw_open_left_over.bend as PAdwOpenLeftOver
import ./proof/admission/adw_step_malformed.bend as PAdwStepMalformed
import ./proof/admission/adw_step_left_over.bend as PAdwStepLeftOver
import ./proof/admission/adw_shut_refuses.bend as PAdwShutRefuses
import ./proof/admission/adw_tags_example.bend as PAdwTagsExample
import ./proof/admission/adw_lim_example.bend as PAdwLimExample
import ./proof/admission/adw_lv_example.bend as PAdwLvExample
import ./proof/admission/adw_lvs_example.bend as PAdwLvsExample
import ./proof/admission/adw_live_example.bend as PAdwLiveExample
import ./proof/admission/adw_op_example.bend as PAdwOpExample
import ./proof/admission/adw_open_example.bend as PAdwOpenExample
import ./proof/admission/adw_malformed_example.bend as PAdwMalformedExample
import ./proof/tree/base/bool.bend as LATreeBool
import ./proof/tree/base/director.bend as LATreeDirector
import ./proof/tree/base/list.bend as LATreeList
import ./proof/tree/base/logic.bend as LATreeLogic
import ./proof/tree/base/maybe.bend as LATreeMaybe
import ./proof/tree/base/nat.bend as LATreeNat
import ./proof/tree/base/pair.bend as LATreePair
import ./proof/tree/base/tree/Ent.bend as LATreeTreeEnt
import ./proof/tree/base/tree/KMap.bend as LATreeTreeKMap
import ./proof/tree/base/tree/above.bend as LATreeTreeAbove
import ./proof/tree/base/tree/core.bend as LATreeTreeCore
import ./proof/tree/base/tree/dels.bend as LATreeTreeDels
import ./proof/tree/base/tree/elem.bend as LATreeTreeElem
import ./proof/tree/base/tree/get.bend as LATreeTreeGet
import ./proof/tree/base/tree/gone.bend as LATreeTreeGone
import ./proof/tree/base/tree/has.bend as LATreeTreeHas
import ./proof/tree/base/tree/ok.bend as LATreeTreeOk
import ./proof/tree/base/tree/put.bend as LATreeTreePut
import ./proof/tree/base/tree/puts.bend as LATreeTreePuts
import ./proof/tree/base/tree/rooted.bend as LATreeTreeRooted
import ./proof/tree/base/tree/same.bend as LATreeTreeSame
import ./proof/tree/base/tree/sorted.bend as LATreeTreeSorted
import ./proof/tree/base/tree/sound.bend as LATreeTreeSound
import ./proof/tree/base/tree/unset.bend as LATreeTreeUnset
import ./proof/tree/base/tree/within.bend as LATreeTreeWithin
import ./proof/tree/base/wire.bend as LATreeWire
import ./proof/tree/tree_apply_sound.bend as PTreeApplySound
import ./proof/tree/tree_replay_sound.bend as PTreeReplaySound
import ./proof/tree/tree_snapshot.bend as PTreeSnapshot
import ./proof/tree/tree_rewind_reaches.bend as PTreeRewindReaches
import ./proof/tree/tree_rewind_still.bend as PTreeRewindStill
import ./proof/tree/tree_rewind_minimal.bend as PTreeRewindMinimal
import ./proof/tree/tree_delete_removes.bend as PTreeDeleteRemoves
import ./proof/tree/tree_delete_only_below.bend as PTreeDeleteOnlyBelow
import ./proof/tree/tree_delete_within.bend as PTreeDeleteWithin
import ./proof/tree/tree_put_sets.bend as PTreePutSets
import ./proof/tree/tree_put_keeps_others.bend as PTreePutKeepsOthers
import ./proof/tree/tree_core_tree.bend as PTreeCoreTree
import ./proof/tree/tree_core_answer.bend as PTreeCoreAnswer
import ./proof/tree/tree_core_note.bend as PTreeCoreNote
import ./proof/tree/tree_core_plan.bend as PTreeCorePlan
import ./proof/tree/tree_core_snap.bend as PTreeCoreSnap
import ./proof/tree/tree_core_plan_keeps.bend as PTreeCorePlanKeeps
import ./proof/tree/tree_core_snap_keeps.bend as PTreeCoreSnapKeeps
import ./proof/tree/dir_encode_sound.bend as PDirEncodeSound
import ./proof/tree/dir_rewind_restores.bend as PDirRewindRestores
import ./proof/tree/tree_ffi_ask_round_trip.bend as PTreeFfiAskRoundTrip
import ./proof/tree/tree_ffi_step.bend as PTreeFfiStep
import ./proof/tree/tree_ffi_malformed.bend as PTreeFfiMalformed
import ./proof/tree/tree_ffi_trailing.bend as PTreeFfiTrailing
import ./proof/tree/tree_ffi_refused.bend as PTreeFfiRefused
import ./proof/tree/tree_ffi_open.bend as PTreeFfiOpen
import ./proof/tree/tree_ffi_open_malformed.bend as PTreeFfiOpenMalformed
import ./proof/tree/tree_ffi_open_trailing.bend as PTreeFfiOpenTrailing
import ./proof/tree/tree_ffi_fits_exists.bend as PTreeFfiFitsExists
import ./proof/tree/tree_ffi_example.bend as PTreeFfiExample
import ./proof/job/base.bend as LAJob
import ./proof/job/job_output_bounded.bend as PJobOutputBounded
import ./proof/job/job_no_silent_loss.bend as PJobNoSilentLoss
import ./proof/job/job_optout_keeps_all.bend as PJobOptoutKeepsAll
import ./proof/job/job_cap_drops_only_excess.bend as PJobCapDropsOnlyExcess
import ./proof/job/job_ends_once.bend as PJobEndsOnce
import ./proof/job/job_end_is_final.bend as PJobEndIsFinal
import ./proof/job/job_kill_ends_now.bend as PJobKillEndsNow
import ./proof/job/call_blocks_at_most_budget.bend as PCallBlocksAtMostBudget
import ./proof/job/call_settles_with_job.bend as PCallSettlesWithJob
import ./proof/job/stream_journals_two.bend as PStreamJournalsTwo
import ./proof/job/stream_settles_once.bend as PStreamSettlesOnce
import ./proof/job/stream_settle_carries_all.bend as PStreamSettleCarriesAll
import ./proof/job/rewind_stops_orphans.bend as PRewindStopsOrphans
import ./proof/job/rewind_keeps_target_jobs.bend as PRewindKeepsTargetJobs
import ./proof/job/job_feed_fits.bend as PJobFeedFits
import ./proof/job/job_feed_no_output.bend as PJobFeedNoOutput
import ./proof/job/job_feed_ended.bend as PJobFeedEnded
import ./proof/job/job_feed_is_a_step.bend as PJobFeedIsAStep
import ./proof/job/job_feed_bounded.bend as PJobFeedBounded
import ./proof/job/job_feed_fills.bend as PJobFeedFills
import ./proof/job/job_entry.bend as PJobEntry
import ./proof/sandbox/base.bend as LASandbox
import ./proof/sandbox/proto_one_reply_each.bend as PProtoOneReplyEach
import ./proof/sandbox/proto_runs_only_accepted.bend as PProtoRunsOnlyAccepted
import ./proof/sandbox/proto_runs_every_accepted.bend as PProtoRunsEveryAccepted
import ./proof/sandbox/proto_rejects_oversize.bend as PProtoRejectsOversize
import ./proof/sandbox/cow_keeps_parent.bend as PCowKeepsParent
import ./proof/sandbox/cow_takes_child.bend as PCowTakesChild
import ./proof/sandbox/cow_conflict_reported.bend as PCowConflictReported
import ./proof/sandbox/cow_conflict_is_real.bend as PCowConflictIsReal
import ./proof/sandbox/cow_plan.bend as PCowPlan
import ./proof/sandbox/cow_plan_is_merge.bend as PCowPlanIsMerge
import ./proof/sandbox/cow_entry.bend as PCowEntry
import ./proof/cvar/base.bend as LACvar
import ./proof/cvar/cvar_registry_unique.bend as PCvarRegistryUnique
import ./proof/cvar/cvar_registry_typed.bend as PCvarRegistryTyped
import ./proof/cvar/cvar_value_typed.bend as PCvarValueTyped
import ./proof/cvar/cvar_inherits.bend as PCvarInherits
import ./proof/cvar/cvar_set_wins.bend as PCvarSetWins
import ./proof/cvar/cvar_global_uniform.bend as PCvarGlobalUniform
import ./proof/cvar/cvar_written_flagged.bend as PCvarWrittenFlagged
import ./proof/cvar/cvar_persist_roundtrip.bend as PCvarPersistRoundtrip
import ./proof/cvar/cvar_toggle_twice.bend as PCvarToggleTwice
import ./proof/cvar/alias_expands_fully.bend as PAliasExpandsFully
import ./proof/cvar/alias_self_cycle.bend as PAliasSelfCycle
import ./proof/cvar/alias_unknown_reported.bend as PAliasUnknownReported
import ./proof/cvar/alias_runs_body.bend as PAliasRunsBody
import ./proof/cvar/alias_expands_in_order.bend as PAliasExpandsInOrder
import ./proof/cvar/alias_expand_example.bend as PAliasExpandExample
import ./proof/cvar/bind_press_plain.bend as PBindPressPlain
import ./proof/cvar/bind_unbound_runs_nothing.bend as PBindUnboundRunsNothing
import ./proof/cvar/bind_first_wins.bend as PBindFirstWins
import ./proof/cvar/cvar_ffi_round_trip.bend as PCvarFfiRoundTrip
import ./proof/cvar/cvar_ffi_is_expand.bend as PCvarFfiIsExpand
import ./proof/cvar/cvar_ffi_malformed.bend as PCvarFfiMalformed
import ./proof/cvar/cvar_ffi_open.bend as PCvarFfiOpen
import ./proof/cvar/cvar_ffi_open_malformed.bend as PCvarFfiOpenMalformed
import ./proof/cvar/cvar_ffi_press.bend as PCvarFfiPress
import ./proof/cvar/cvar_ffi_refused.bend as PCvarFfiRefused
import ./proof/cvar/cvar_fits_example.bend as PCvarFitsExample
import ./proof/director/base.bend as LADirector
import ./proof/director/dir_stack_bounded.bend as PDirStackBounded
import ./proof/director/dir_loop_stack_bounded.bend as PDirLoopStackBounded
import ./proof/director/dir_loop_ends.bend as PDirLoopEnds
import ./proof/director/dir_end_is_final.bend as PDirEndIsFinal
import ./proof/director/dir_resume_restores.bend as PDirResumeRestores
import ./proof/director/dir_go_empty.bend as PDirGoEmpty
import ./proof/director/dir_go_unjudged.bend as PDirGoUnjudged
import ./proof/director/dir_go_defer.bend as PDirGoDefer
import ./proof/director/dir_go_leave.bend as PDirGoLeave
import ./proof/director/dir_go_lead_stays.bend as PDirGoLeadStays
import ./proof/director/dir_go_lead_leaves.bend as PDirGoLeadLeaves
import ./proof/director/dir_go_yield.bend as PDirGoYield
import ./proof/director/dir_go_abort.bend as PDirGoAbort
import ./proof/director/dir_go_again.bend as PDirGoAgain
import ./proof/director/dir_go_again_spent.bend as PDirGoAgainSpent
import ./proof/director/dir_go_push.bend as PDirGoPush
import ./proof/director/dir_go_push_full.bend as PDirGoPushFull
import ./proof/director/dir_go_push_spent.bend as PDirGoPushSpent
import ./proof/director/dir_room.bend as PDirRoom
import ./proof/director/dir_decide_goes_on.bend as PDirDecideGoesOn
import ./proof/director/dir_tick_goes_on.bend as PDirTickGoesOn
import ./proof/director/dir_tick_out_of_steps.bend as PDirTickOutOfSteps
import ./proof/director/dir_tick_hands_back.bend as PDirTickHandsBack
import ./proof/director/dir_tick_fails.bend as PDirTickFails
import ./proof/director/dir_lead_leaves_with_the_continuation.bend as PDirLeadLeavesWithTheContinuation
import ./proof/director/dir_lead_stays_when_the_loop_ends.bend as PDirLeadStaysWhenTheLoopEnds
import ./proof/director/dir_lead_goes_example.bend as PDirLeadGoesExample
import ./proof/director/dir_lead_stays_example.bend as PDirLeadStaysExample
import ./proof/director/dir_ffi_round_trip.bend as PDirFfiRoundTrip
import ./proof/director/dir_ffi_is_tick.bend as PDirFfiIsTick
import ./proof/director/dir_ffi_malformed.bend as PDirFfiMalformed
import ./proof/director/dir_ffi_left_over.bend as PDirFfiLeftOver
import ./proof/director/dir_req_fits_example.bend as PDirReqFitsExample
import ./proof/infer/base.bend as LAInfer
import ./proof/infer/quirk_unknown_rejected.bend as PQuirkUnknownRejected
import ./proof/infer/quirk_clash_rejected.bend as PQuirkClashRejected
import ./proof/infer/quirk_unknown_when_none.bend as PQuirkUnknownWhenNone
import ./proof/infer/quirk_known_when_some.bend as PQuirkKnownWhenSome
import ./proof/infer/quirk_highest_wins.bend as PQuirkHighestWins
import ./proof/infer/quirk_order_free.bend as PQuirkOrderFree
import ./proof/infer/quirk_compile_order_free.bend as PQuirkCompileOrderFree
import ./proof/infer/force_bounded.bend as PForceBounded
import ./proof/infer/force_first_flag.bend as PForceFirstFlag
import ./proof/infer/force_retry_flag.bend as PForceRetryFlag
import ./proof/infer/force_reports.bend as PForceReports
import ./proof/infer/strict_within_cap.bend as PStrictWithinCap
import ./proof/infer/strict_keeps_every_tool.bend as PStrictKeepsEveryTool
import ./proof/infer/strict_by_priority.bend as PStrictByPriority
import ./proof/infer/strict_no_cap.bend as PStrictNoCap
import ./proof/infer/strict_cap_is_strict.bend as PStrictCapIsStrict
import ./proof/infer/plan_fits_lists_the_loose.bend as PPlanFitsListsTheLoose
import ./proof/infer/plan_never_loosens_a_needed_tool.bend as PPlanNeverLoosensANeededTool
import ./proof/infer/plan_refusal_names_a_needed_loose_tool.bend as PPlanRefusalNamesANeededLooseTool
import ./proof/infer/plan_example_over.bend as PPlanExampleOver
import ./proof/infer/plan_example_fits.bend as PPlanExampleFits
import ./proof/infer/guard_cuts_repeats.bend as PGuardCutsRepeats
import ./proof/infer/guard_cuts_loops.bend as PGuardCutsLoops
import ./proof/infer/guard_keeps_others.bend as PGuardKeepsOthers
import ./proof/infer/compact_starts_early.bend as PCompactStartsEarly
import ./proof/infer/quirk_ladder_explicit_first.bend as PQuirkLadderExplicitFirst
import ./proof/infer/quirk_ladder_rule_second.bend as PQuirkLadderRuleSecond
import ./proof/infer/quirk_ladder_default_last.bend as PQuirkLadderDefaultLast
import ./proof/infer/quirk_ladder_shipped_is_s10.bend as PQuirkLadderShippedIsS10
import ./proof/infer/quirk_ladder_reasons.bend as PQuirkLadderReasons
import ./proof/infer/core_infer_round_trip.bend as PCoreInferRoundTrip
import ./proof/infer/core_infer_answers.bend as PCoreInferAnswers
import ./proof/infer/core_infer_malformed.bend as PCoreInferMalformed
import ./proof/infer/core_infer_left_over.bend as PCoreInferLeftOver
import ./proof/infer/core_infer_req_example.bend as PCoreInferReqExample
import ./proof/infer/core_infer_reply_example.bend as PCoreInferReplyExample
import ./proof/infer/core_infer_malformed_example.bend as PCoreInferMalformedExample
import ./proof/infer/facts_rulebook_decides.bend as PFactsRulebookDecides
import ./proof/infer/facts_rulebook_default.bend as PFactsRulebookDefault
import ./proof/infer/facts_only_the_rulebook_decides.bend as PFactsOnlyTheRulebookDecides
import ./proof/tools/base.bend as LATools
import ./proof/tools/roster_fixed.bend as PRosterFixed
import ./proof/tools/roster_sent_fixed.bend as PRosterSentFixed
import ./proof/tools/dyn_reaches_joined.bend as PDynReachesJoined
import ./proof/tools/dyn_drops_quit.bend as PDynDropsQuit
import ./proof/tools/schema_has_intent.bend as PSchemaHasIntent
import ./proof/tools/schema_versioned.bend as PSchemaVersioned
import ./proof/tools/schema_keeps_params.bend as PSchemaKeepsParams
import ./proof/tools/schema_build_idempotent.bend as PSchemaBuildIdempotent
import ./proof/tools/path_rejects_escape.bend as PPathRejectsEscape
import ./proof/tools/path_resolves_inside.bend as PPathResolvesInside
import ./proof/tools/tools_ffi_request_round_trip.bend as PToolsFfiRequestRoundTrip
import ./proof/tools/tools_ffi_answers.bend as PToolsFfiAnswers
import ./proof/tools/tools_ffi_rejects_malformed.bend as PToolsFfiRejectsMalformed
import ./proof/tools/tools_ffi_rejects_left_over.bend as PToolsFfiRejectsLeftOver
import ./proof/tools/gate_prefix.bend as PGatePrefix
import ./proof/tools/gate_needs_yes.bend as PGateNeedsYes
import ./proof/tools/gate_deny_stops.bend as PGateDenyStops
import ./proof/tools/gate_finish_runs_all.bend as PGateFinishRunsAll
import ./proof/tools/gate_inside_write_runs.bend as PGateInsideWriteRuns
import ./proof/tools/step_holds_every_part.bend as PStepHoldsEveryPart
import ./proof/tools/secret_needs_a_secret_path.bend as PSecretNeedsASecretPath
import ./proof/tools/secret_path_gives_secret.bend as PSecretPathGivesSecret
import ./proof/tools/auto_needs_every_effect.bend as PAutoNeedsEveryEffect
import ./proof/tools/auto_never_sensitive.bend as PAutoNeverSensitive
import ./proof/tools/composed_needs_every_part.bend as PComposedNeedsEveryPart
import ./proof/tools/auto_runs_within.bend as PAutoRunsWithin
import ./proof/tools/held_needs_a_yes.bend as PHeldNeedsAYes
import ./proof/tools/gateway_refuses_protected.bend as PGatewayRefusesProtected
import ./proof/tools/gateway_refuses_secret.bend as PGatewayRefusesSecret
import ./proof/tools/gateway_runs_the_rest.bend as PGatewayRunsTheRest
import ./proof/tools/default_auto_is_grantable.bend as PDefaultAutoIsGrantable
import ./proof/tools/never_auto_is_routed.bend as PNeverAutoIsRouted
import ./proof/tools/never_auto_asks_the_client.bend as PNeverAutoAsksTheClient
import ./proof/tools/outside_runs_only_by_the_gateway.bend as POutsideRunsOnlyByTheGateway
import ./proof/tools/guarded_refused_from_the_phone.bend as PGuardedRefusedFromThePhone
import ./proof/screen/base.bend as LAScreen
import ./proof/screen/tx_gapless.bend as PTxGapless
import ./proof/screen/tx_scrollback_append_only.bend as PTxScrollbackAppendOnly
import ./proof/screen/tx_resize_keeps.bend as PTxResizeKeeps
import ./proof/screen/tx_flush_settles.bend as PTxFlushSettles
import ./proof/screen/pace_never_ahead.bend as PPaceNeverAhead
import ./proof/screen/pace_never_back.bend as PPaceNeverBack
import ./proof/screen/pace_drains.bend as PPaceDrains
import ./proof/screen/verify_only_checked.bend as PVerifyOnlyChecked
import ./proof/screen/paint_first_passing_check.bend as PPaintFirstPassingCheck
import ./proof/screen/layout_inside.bend as PLayoutInside
import ./proof/screen/layout_apart.bend as PLayoutApart
import ./proof/screen/layout_whole_when_room.bend as PLayoutWholeWhenRoom
import ./proof/screen/pace_reveal_formula.bend as PPaceRevealFormula
import ./proof/screen/pace_lag_at_cap.bend as PPaceLagAtCap
import ./proof/screen/tx_committed_inert.bend as PTxCommittedInert
import ./proof/screen/all_comm_example.bend as PAllCommExample
import ./proof/screen/all_comm_rejects.bend as PAllCommRejects
import ./proof/screen/rec_length_retries_with_a_note.bend as PRecLengthRetriesWithANote
import ./proof/screen/rec_leak_retries_with_a_note.bend as PRecLeakRetriesWithANote
import ./proof/screen/screen_ffi_run.bend as PScreenFfiRun
import ./proof/screen/screen_ffi_pace.bend as PScreenFfiPace
import ./proof/screen/screen_ffi_stack.bend as PScreenFfiStack
import ./proof/screen/screen_ffi_example.bend as PScreenFfiExample
import ./proof/screen/screen_ffi_refuses_example.bend as PScreenFfiRefusesExample
import ./proof/screen/screen_ffi_paint.bend as PScreenFfiPaint
import ./proof/screen/screen_ffi_paint_example.bend as PScreenFfiPaintExample
import ./proof/tiny/base.bend as LATiny
import ./proof/tiny/tiny_pick_in_chain.bend as PTinyPickInChain
import ./proof/tiny/tiny_pick_first.bend as PTinyPickFirst
import ./proof/tiny/tiny_pick_unavailable.bend as PTinyPickUnavailable
import ./proof/tiny/tiny_every_need_served.bend as PTinyEveryNeedServed
import ./proof/tiny/tiny_worker_current.bend as PTinyWorkerCurrent
import ./proof/tiny/tiny_same_tag_joins.bend as PTinySameTagJoins
import ./proof/tiny/tiny_ffi_request_round_trip.bend as PTinyFfiRequestRoundTrip
import ./proof/tiny/tiny_ffi_answers.bend as PTinyFfiAnswers
import ./proof/tiny/tiny_ffi_rejects_malformed.bend as PTinyFfiRejectsMalformed
import ./proof/tiny/tiny_ffi_rejects_left_over.bend as PTinyFfiRejectsLeftOver
import ./proof/tiny/tiny_elect_spec.bend as PTinyElectSpec
import ./proof/tiny/tiny_shut_spec.bend as PTinyShutSpec
import ./proof/tiny/tiny_launched_spec.bend as PTinyLaunchedSpec
import ./proof/tiny/tiny_confirm_spec.bend as PTinyConfirmSpec
import ./proof/tiny/tiny_bind_spec.bend as PTinyBindSpec
import ./proof/tiny/tiny_elect_is_worker_model.bend as PTinyElectIsWorkerModel
import ./proof/tiny/tiny_elect_entry_answers.bend as PTinyElectEntryAnswers
import ./proof/tiny/tiny_elect_entry_reads.bend as PTinyElectEntryReads
import ./proof/tiny/tiny_elect_entry_exact.bend as PTinyElectEntryExact
import ./proof/tiny/tiny_elect_entry_refuses.bend as PTinyElectEntryRefuses
import ./proof/tiny/tiny_elect_entry_example.bend as PTinyElectEntryExample
import ./proof/effort/base.bend as LAEffort
import ./proof/effort/effort_offered_plain.bend as PEffortOfferedPlain
import ./proof/effort/effort_offered_null.bend as PEffortOfferedNull
import ./proof/effort/effort_offered_ext.bend as PEffortOfferedExt
import ./proof/effort/effort_offered_kept.bend as PEffortOfferedKept
import ./proof/effort/effort_offered_asc.bend as PEffortOfferedAsc
import ./proof/effort/effort_clamp_offered.bend as PEffortClampOffered
import ./proof/effort/effort_clamp_keeps.bend as PEffortClampKeeps
import ./proof/effort/effort_clamp_idem.bend as PEffortClampIdem
import ./proof/effort/effort_cycle_still.bend as PEffortCycleStill
import ./proof/effort/effort_cycle_next.bend as PEffortCycleNext
import ./proof/effort/effort_cycle_wrap.bend as PEffortCycleWrap
import ./proof/effort/effort_cycle_prev.bend as PEffortCyclePrev
import ./proof/effort/effort_cycle_wrap_back.bend as PEffortCycleWrapBack
import ./proof/effort/effort_cycle_inverse.bend as PEffortCycleInverse
import ./proof/effort/effort_cycle_inverse_back.bend as PEffortCycleInverseBack
import ./proof/effort/effort_unset_default.bend as PEffortUnsetDefault
import ./proof/effort/effort_settle_offered.bend as PEffortSettleOffered
import ./proof/effort/effort_stored_is_sent.bend as PEffortStoredIsSent
import ./proof/effort/effort_shown_is_sent.bend as PEffortShownIsSent
import ./proof/effort/quirk_ladder_offered_exact.bend as PQuirkLadderOfferedExact
import ./proof/effort/quirk_ladder_plain_exact.bend as PQuirkLadderPlainExact
import ./proof/effort/quirk_ladder_model_offers.bend as PQuirkLadderModelOffers
import ./proof/effort/core_effort_round_trip.bend as PCoreEffortRoundTrip
import ./proof/effort/core_effort_offered.bend as PCoreEffortOffered
import ./proof/effort/core_effort_clamp.bend as PCoreEffortClamp
import ./proof/effort/core_effort_cycle.bend as PCoreEffortCycle
import ./proof/effort/core_effort_malformed.bend as PCoreEffortMalformed
import ./proof/effort/core_effort_left_over.bend as PCoreEffortLeftOver
import ./proof/effort/core_effort_req_example.bend as PCoreEffortReqExample
import ./proof/effort/core_effort_reply_example.bend as PCoreEffortReplyExample
import ./proof/effort/core_effort_malformed_example.bend as PCoreEffortMalformedExample
import ./proof/run/base.bend as LARun
import ./proof/run/run_ends.bend as PRunEnds
import ./proof/run/run_end_stays.bend as PRunEndStays
import ./proof/run/run_abort_ends_now.bend as PRunAbortEndsNow
import ./proof/run/run_rounds_capped.bend as PRunRoundsCapped
import ./proof/run/run_rounds_fail_at_cap.bend as PRunRoundsFailAtCap
import ./proof/run/run_polls_need_defers.bend as PRunPollsNeedDefers
import ./proof/run/run_no_answer_is_an_error.bend as PRunNoAnswerIsAnError
import ./proof/run/run_calls_never_answer.bend as PRunCallsNeverAnswer
import ./proof/run/run_note_spends_no_retry.bend as PRunNoteSpendsNoRetry
import ./proof/run/run_retry_spends_no_note.bend as PRunRetrySpendsNoNote
import ./proof/run/run_retry_sends_a_new_request.bend as PRunRetrySendsANewRequest
import ./proof/run/run_cut_names_the_request.bend as PRunCutNamesTheRequest
import ./proof/run/run_note_is_never_logged.bend as PRunNoteIsNeverLogged
import ./proof/run/run_reply_is_the_rust_rule.bend as PRunReplyIsTheRustRule
import ./proof/run/run_prepare_is_the_rust_rule.bend as PRunPrepareIsTheRustRule
import ./proof/run/run_prepare_compacted_reads_no_threshold.bend as PRunPrepareCompactedReadsNoThreshold
import ./proof/run/run_compact_is_the_rust_rule.bend as PRunCompactIsTheRustRule
import ./proof/run/run_round_is_the_rust_rule.bend as PRunRoundIsTheRustRule
import ./proof/run/run_round_counts_down.bend as PRunRoundCountsDown
import ./proof/run/run_note_counts_down.bend as PRunNoteCountsDown
import ./proof/run/run_note_keeps_the_retries.bend as PRunNoteKeepsTheRetries
import ./proof/run/run_retry_counts_down.bend as PRunRetryCountsDown
import ./proof/run/run_retry_premise_witness.bend as PRunRetryPremiseWitness
import ./proof/run/run_retry_keeps_the_notes.bend as PRunRetryKeepsTheNotes
import ./proof/run/run_counts_lossless.bend as PRunCountsLossless
import ./proof/run/run_counts_within_witness.bend as PRunCountsWithinWitness
import ./proof/run/run_rounds_lossless.bend as PRunRoundsLossless
import ./proof/run/run_rounds_within_witness.bend as PRunRoundsWithinWitness
import ./proof/run/run_failed_poll_is_the_job_model.bend as PRunFailedPollIsTheJobModel
import ./proof/run/run_deferred_reply_is_the_job_model.bend as PRunDeferredReplyIsTheJobModel
import ./proof/run/run_first_deferred_reply_is_the_job_model.bend as PRunFirstDeferredReplyIsTheJobModel
import ./proof/run/run_reply_saturates_the_wait.bend as PRunReplySaturatesTheWait
import ./proof/run/run_reply_saturates_the_attempt.bend as PRunReplySaturatesTheAttempt
import ./proof/run/rec_length_gives_up.bend as PRecLengthGivesUp
import ./proof/run/rec_leak_rebuilt_is_calls.bend as PRecLeakRebuiltIsCalls
import ./proof/run/rec_leak_stands.bend as PRecLeakStands
import ./proof/run/rec_calls_run.bend as PRecCallsRun
import ./proof/run/rec_repeat_never_runs.bend as PRecRepeatNeverRuns
import ./proof/run/rec_repeat_redirects.bend as PRecRepeatRedirects
import ./proof/run/rec_repeat_gives_up.bend as PRecRepeatGivesUp
import ./proof/run/rec_user_breaks_the_row.bend as PRecUserBreaksTheRow
import ./proof/run/rec_notes_capped.bend as PRecNotesCapped
import ./proof/run/rec_never_runs_a_repeat.bend as PRecNeverRunsARepeat
import ./proof/run/rec_stuck_gets_help.bend as PRecStuckGetsHelp
import ./proof/run/rec_redo_is_noted.bend as PRecRedoIsNoted
import ./proof/run/rec_quit_fails.bend as PRecQuitFails
import ./proof/run/rec_recover_is_the_rust_rule.bend as PRecRecoverIsTheRustRule
import ./proof/run/run_ffi_ask_round_trip.bend as PRunFfiAskRoundTrip
import ./proof/run/run_ffi_ask_fits_witness.bend as PRunFfiAskFitsWitness
import ./proof/run/run_ffi_answers.bend as PRunFfiAnswers
import ./proof/run/run_ffi_refuses_left_over.bend as PRunFfiRefusesLeftOver
import ./proof/run/run_ffi_left_over_witness.bend as PRunFfiLeftOverWitness
import ./proof/run/run_ffi_refuses_malformed.bend as PRunFfiRefusesMalformed
import ./proof/run/run_ffi_malformed_witness.bend as PRunFfiMalformedWitness
import ./proof/run/run_ffi_then_round_trip.bend as PRunFfiThenRoundTrip
import ./proof/run/run_ffi_prepared_round_trip.bend as PRunFfiPreparedRoundTrip
import ./proof/run/run_ffi_end_round_trip.bend as PRunFfiEndRoundTrip
import ./proof/run/run_ffi_help_round_trip.bend as PRunFfiHelpRoundTrip
import ./proof/run/run_ffi_reply_round_trip.bend as PRunFfiReplyRoundTrip
import ./proof/run/run_ffi_answer_fits_witness.bend as PRunFfiAnswerFitsWitness
import ./proof/semver/base.bend as LASemver
import ./proof/semver/semver_roundtrip.bend as PSemverRoundtrip
import ./proof/semver/semver_le_refl.bend as PSemverLeRefl
import ./proof/semver/semver_le_antisym.bend as PSemverLeAntisym
import ./proof/semver/semver_le_trans.bend as PSemverLeTrans
import ./proof/semver/semver_le_total.bend as PSemverLeTotal
import ./proof/semver/semver_le_exact.bend as PSemverLeExact
import ./proof/semver/semver_next_newer.bend as PSemverNextNewer
import ./proof/semver/semver_next_not_tagged.bend as PSemverNextNotTagged
import ./proof/semver/semver_next_tag_new.bend as PSemverNextTagNew
import ./proof/semver/semver_fresh_series.bend as PSemverFreshSeries
import ./proof/semver/semver_other_series.bend as PSemverOtherSeries
import ./proof/semver/semver_title.bend as PSemverTitle
import ./proof/semver/semver_tag_roundtrip.bend as PSemverTagRoundtrip
import ./proof/semver/semver_release_newest.bend as PSemverReleaseNewest
import ./proof/semver/semver_release_progress.bend as PSemverReleaseProgress
import ./proof/semver/semver_release_refuses_patch_workspace.bend as PSemverReleaseRefusesPatchWorkspace
import ./proof/semver/semver_release_refuses_unparsed_workspace.bend as PSemverReleaseRefusesUnparsedWorkspace
import ./proof/semver/semver_parse_patch_example.bend as PSemverParsePatchExample
import ./proof/semver/semver_parse_two_fields_example.bend as PSemverParseTwoFieldsExample
import ./proof/semver/semver_show_decimal.bend as PSemverShowDecimal
import ./proof/semver/semver_dec_spec_example.bend as PSemverDecSpecExample
import ./proof/semver/semver_parse_exact.bend as PSemverParseExact
import ./proof/semver/semver_in_series_exact.bend as PSemverInSeriesExact
import ./proof/semver/semver_next_exact.bend as PSemverNextExact
import ./proof/semver/semver_release_exact.bend as PSemverReleaseExact
import ./proof/semver/semver_ffi_release.bend as PSemverFfiRelease
import ./proof/semver/semver_ffi_release_long.bend as PSemverFfiReleaseLong
import ./proof/semver/semver_ffi_series.bend as PSemverFfiSeries
import ./proof/semver/semver_ffi_series_long.bend as PSemverFfiSeriesLong
import ./proof/semver/semver_ffi_exact.bend as PSemverFfiExact
import ./proof/semver/semver_ffi_exact_fits.bend as PSemverFfiExactFits
import ./proof/semver/semver_ffi_release_example.bend as PSemverFfiReleaseExample
import ./proof/semver/semver_ffi_behind_example.bend as PSemverFfiBehindExample
import ./proof/semver/semver_ffi_why_example.bend as PSemverFfiWhyExample
import ./proof/semver/semver_ffi_series_example.bend as PSemverFfiSeriesExample
import ./proof/semver/semver_ffi_long_example.bend as PSemverFfiLongExample
import ./proof/semver/semver_ffi_malformed_example.bend as PSemverFfiMalformedExample
import ./proof/semver/replace_rank_in_range.bend as PReplaceRankInRange
import ./proof/auth_flight/base.bend as LAAuthFlight
import ./proof/auth_flight/flight_one_fetch.bend as PFlightOneFetch
import ./proof/auth_flight/flight_board_joins.bend as PFlightBoardJoins
import ./proof/auth_flight/flight_callers_get_its_outcome.bend as PFlightCallersGetItsOutcome
import ./proof/auth_flight/flight_landed_serves.bend as PFlightLandedServes
import ./proof/auth_flight/flight_after_end_stored.bend as PFlightAfterEndStored
import ./proof/auth_flight/flight_after_end_served.bend as PFlightAfterEndServed
import ./proof/auth_flight/flight_board_leads.bend as PFlightBoardLeads
import ./proof/auth_flight/flight_terms_exact.bend as PFlightTermsExact
import ./proof/auth_flight/flight_land_ends.bend as PFlightLandEnds
import ./proof/auth_flight/flight_step_exact.bend as PFlightStepExact
import ./proof/auth_flight/flight_new_example.bend as PFlightNewExample
import ./proof/auth_flight/flight_store_terms_exact.bend as PFlightStoreTermsExact
import ./proof/auth_flight/base/entry.bend as LAAuthFlightEntry
import ./proof/auth_flight/flight_ffi_answers.bend as PFlightFfiAnswers
import ./proof/auth_flight/flight_ffi_reads.bend as PFlightFfiReads
import ./proof/auth_flight/flight_ffi_malformed_exact.bend as PFlightFfiMalformedExact
import ./proof/auth_flight/flight_ffi_example.bend as PFlightFfiExample
import ./proof/auth_flight/flight_next_load_is_model.bend as PFlightNextLoadIsModel
import ./proof/auth_flight/flight_next_check_is_model.bend as PFlightNextCheckIsModel
import ./proof/auth_flight/flight_next_fetch_is_model.bend as PFlightNextFetchIsModel
import ./proof/auth_flight/flight_next_store_is_model.bend as PFlightNextStoreIsModel
import ./proof/auth_flight/flight_open_empty.bend as PFlightOpenEmpty
import ./proof/auth_flight/flight_open_refuses.bend as PFlightOpenRefuses
import ./proof/auth_flight/flight_step_answers.bend as PFlightStepAnswers
import ./proof/auth_flight/flight_step_reads.bend as PFlightStepReads
import ./proof/auth_flight/flight_step_malformed_exact.bend as PFlightStepMalformedExact
import ./proof/auth_flight/flight_step_example.bend as PFlightStepExample
import ./proof/theme/base.bend as LATheme
import ./proof/theme/theme_resolve_empty.bend as PThemeResolveEmpty
import ./proof/theme/theme_resolve_first.bend as PThemeResolveFirst
import ./proof/theme/theme_resolve_missing.bend as PThemeResolveMissing
import ./proof/theme/theme_load_valid.bend as PThemeLoadValid
import ./proof/theme/theme_tokens_complete.bend as PThemeTokensComplete
import ./proof/theme/theme_mode_background.bend as PThemeModeBackground
import ./proof/theme/theme_palette_name_free.bend as PThemePaletteNameFree
import ./proof/theme/theme_mode_name_free.bend as PThemeModeNameFree
import ./proof/theme/theme_shipped_legible.bend as PThemeShippedLegible
import ./proof/theme/theme_shipped_status_distinct.bend as PThemeShippedStatusDistinct
import ./proof/theme/theme_chase_rule.bend as PThemeChaseRule
import ./proof/theme/theme_chase_example.bend as PThemeChaseExample
import ./proof/theme/theme_entry_unknown.bend as PThemeEntryUnknown
import ./proof/theme/theme_entry_color.bend as PThemeEntryColor
import ./proof/theme/theme_entry_invalid.bend as PThemeEntryInvalid
import ./proof/theme/theme_read_first_error.bend as PThemeReadFirstError
import ./proof/theme/theme_required_tokens.bend as PThemeRequiredTokens
import ./proof/theme/theme_read_missing.bend as PThemeReadMissing
import ./proof/theme/theme_read_page.bend as PThemeReadPage
import ./proof/theme/theme_read_card.bend as PThemeReadCard
import ./proof/theme/theme_read_info.bend as PThemeReadInfo
import ./proof/theme/theme_read_loaded.bend as PThemeReadLoaded
import ./proof/theme/theme_parse_rejected.bend as PThemeParseRejected
import ./proof/theme/theme_parse_painted.bend as PThemeParsePainted
import ./proof/theme/theme_palette_tokens.bend as PThemePaletteTokens
import ./proof/theme/theme_fill_required.bend as PThemeFillRequired
import ./proof/theme/theme_fill_md.bend as PThemeFillMd
import ./proof/theme/theme_fill_refinement.bend as PThemeFillRefinement
import ./proof/theme/theme_fill_canvas.bend as PThemeFillCanvas
import ./proof/theme/theme_defaults_shipped.bend as PThemeDefaultsShipped
import ./proof/theme/theme_background_order.bend as PThemeBackgroundOrder
import ./proof/theme/theme_pick_res.bend as PThemePickRes
import ./proof/theme/theme_pick_cause.bend as PThemePickCause
import ./proof/theme/theme_pick_quiet.bend as PThemePickQuiet
import ./proof/theme/theme_pick_broken.bend as PThemePickBroken
import ./proof/theme/theme_pick_clashes.bend as PThemePickClashes
import ./proof/theme/theme_pick_example.bend as PThemePickExample
import ./proof/theme/tui_roles_resolve.bend as PTuiRolesResolve
import ./proof/color/theme_hex_example.bend as PThemeHexExample
import ./proof/color/theme_hex_digits.bend as PThemeHexDigits
import ./proof/color/theme_hex_value.bend as PThemeHexValue
import ./proof/color/theme_hex_shape.bend as PThemeHexShape
import ./proof/color/theme_num_bytes.bend as PThemeNumBytes
import ./proof/color/theme_num_bytes_128.bend as PThemeNumBytes128
import ./proof/color/theme_num_example.bend as PThemeNumExample
import ./proof/color/theme_to256_palette_16.bend as PThemeTo256Palette16
import ./proof/color/theme_to256_palette_76.bend as PThemeTo256Palette76
import ./proof/color/theme_to256_palette_136.bend as PThemeTo256Palette136
import ./proof/color/theme_to256_palette_196.bend as PThemeTo256Palette196
import ./proof/color/theme_contrast_example.bend as PThemeContrastExample
import ./proof/tokens/tokens_paired.bend as PTokensPaired
import ./proof/tokens/tokens_legible.bend as PTokensLegible
import ./proof/tokens/tokens_layers_ordered.bend as PTokensLayersOrdered
import ./proof/tokens/tokens_space_ascends.bend as PTokensSpaceAscends
import ./proof/tokens/tokens_type_ascends.bend as PTokensTypeAscends
import ./proof/tokens/tokens_ffi_blocks.bend as PTokensFfiBlocks
import ./proof/tokens/tokens_ffi_malformed_exact.bend as PTokensFfiMalformedExact
import ./proof/tokens/tokens_ffi_example.bend as PTokensFfiExample
import ./proof/tokens/tokens_palette_tones.bend as PTokensPaletteTones
import ./proof/tokens/tokens_ascends_exact.bend as PTokensAscendsExact
import ./proof/tokens/tokens_find_exact.bend as PTokensFindExact
import ./proof/tokens/tokens_readable_exact.bend as PTokensReadableExact
import ./proof/tokens/tokens_pairs_exact.bend as PTokensPairsExact
import ./proof/tokens/tokens_ink_opaque.bend as PTokensInkOpaque
import ./proof/tokens/tokens_names_exact.bend as PTokensNamesExact
import ./proof/tokens/tokens_channels_in_range.bend as PTokensChannelsInRange
import ./proof/tokens/tokens_scale_keys_distinct.bend as PTokensScaleKeysDistinct
import ./proof/tokens/tokens_scale_keys_plain.bend as PTokensScaleKeysPlain
import ./proof/tokens/tokens_alpha_visible.bend as PTokensAlphaVisible
import ./proof/tokens/tokens_layers_in_range.bend as PTokensLayersInRange
import ./proof/tokens/tokens_px_in_range.bend as PTokensPxInRange
import ./proof/tokens/tokens_type_in_range.bend as PTokensTypeInRange
import ./proof/progress/base.bend as LAProgress
import ./proof/progress/child_repeat_is_no_work.bend as PChildRepeatIsNoWork
import ./proof/progress/child_loop_is_a_stall.bend as PChildLoopIsAStall
import ./proof/progress/child_new_work_is_progress.bend as PChildNewWorkIsProgress
import ./proof/progress/goal_stops_without_progress.bend as PGoalStopsWithoutProgress
import ./proof/progress/goal_progress_continues.bend as PGoalProgressContinues
import ./proof/progress/goal_first_check_starts.bend as PGoalFirstCheckStarts
import ./proof/progress/goal_judge_is_check.bend as PGoalJudgeIsCheck
import ./proof/progress/goal_judge_counts_work.bend as PGoalJudgeCountsWork
import ./proof/progress/goal_judge_held.bend as PGoalJudgeHeld
import ./proof/progress/goal_judge_top_stops.bend as PGoalJudgeTopStops
import ./proof/progress/goal_entry.bend as PGoalEntry
import ./proof/aux_fallback/base.bend as LAAuxFallback
import ./proof/aux_fallback/fallback_is_reported.bend as PFallbackIsReported
import ./proof/aux_fallback/fallback_quiet_when_routed.bend as PFallbackQuietWhenRouted
import ./proof/aux_fallback/fallback_quiet_when_unset.bend as PFallbackQuietWhenUnset
import ./proof/aux_fallback/fallback_quiet_when_same.bend as PFallbackQuietWhenSame
import ./proof/aux_fallback/fallback_gate_then_settle.bend as PFallbackGateThenSettle
import ./proof/aux_fallback/fallback_known_needs_no_lookup.bend as PFallbackKnownNeedsNoLookup
import ./proof/aux_fallback/fallback_gate_other.bend as PFallbackGateOther
import ./proof/aux_fallback/fallback_gate_session.bend as PFallbackGateSession
import ./proof/aux_fallback/fallback_miss_keeps_reason.bend as PFallbackMissKeepsReason
import ./proof/aux_fallback/fallback_window_fits.bend as PFallbackWindowFits
import ./proof/aux_fallback/fallback_window_small.bend as PFallbackWindowSmall
import ./proof/aux_fallback/fallback_pass_events.bend as PFallbackPassEvents
import ./proof/aux_fallback/afw_ev_round_trip.bend as PAfwEvRoundTrip
import ./proof/aux_fallback/afw_evs_round_trip.bend as PAfwEvsRoundTrip
import ./proof/aux_fallback/afw_pass_round_trip.bend as PAfwPassRoundTrip
import ./proof/aux_fallback/afw_answers_gate.bend as PAfwAnswersGate
import ./proof/aux_fallback/afw_answers_settle.bend as PAfwAnswersSettle
import ./proof/aux_fallback/afw_answers_pass.bend as PAfwAnswersPass
import ./proof/aux_fallback/afw_malformed.bend as PAfwMalformed
import ./proof/aux_fallback/afw_left_over.bend as PAfwLeftOver
import ./proof/aux_fallback/afw_key_example.bend as PAfwKeyExample
import ./proof/aux_fallback/afw_keys_example.bend as PAfwKeysExample
import ./proof/aux_fallback/afw_route_example.bend as PAfwRouteExample
import ./proof/aux_fallback/afw_gate_example.bend as PAfwGateExample
import ./proof/aux_fallback/afw_sel_example.bend as PAfwSelExample
import ./proof/aux_fallback/afw_look_example.bend as PAfwLookExample
import ./proof/aux_fallback/afw_ev_example.bend as PAfwEvExample
import ./proof/aux_fallback/afw_evs_example.bend as PAfwEvsExample
import ./proof/aux_fallback/afw_gate_req_example.bend as PAfwGateReqExample
import ./proof/aux_fallback/afw_settle_req_example.bend as PAfwSettleReqExample
import ./proof/aux_fallback/afw_pass_req_example.bend as PAfwPassReqExample
import ./proof/aux_fallback/afw_pass_example.bend as PAfwPassExample
import ./proof/aux_fallback/afw_ffi_example.bend as PAfwFfiExample
import ./proof/aux_fallback/afw_malformed_example.bend as PAfwMalformedExample
import ./proof/skill_load/skill_failure_reported.bend as PSkillFailureReported
import ./proof/skill_load/skill_loaded_not_failed.bend as PSkillLoadedNotFailed
import ./proof/skill_load/base.bend as LASkillLoad
import ./proof/skill_load/skill_ffi_answers.bend as PSkillFfiAnswers
import ./proof/skill_load/skill_ffi_malformed.bend as PSkillFfiMalformed
import ./proof/skill_load/skill_ffi_example.bend as PSkillFfiExample
import ./proof/skill_load/skill_diag_kinds.bend as PSkillDiagKinds
import ./proof/skill_load/skill_distinct_example.bend as PSkillDistinctExample
import ./proof/skill_load/skill_ffi_malformed_exact.bend as PSkillFfiMalformedExact
import ./proof/skill_load/skill_loaded_exact.bend as PSkillLoadedExact
import ./proof/skill_load/skill_in_first_example.bend as PSkillInFirstExample
import ./proof/skill_load/skill_in_later_example.bend as PSkillInLaterExample
import ./proof/kernel_local/kernel_session_never_downloads.bend as PKernelSessionNeverDownloads
import ./proof/kernel_local/kernel_download_only_on_install.bend as PKernelDownloadOnlyOnInstall
import ./proof/kernel_local/kernel_fetch_verified_before_use.bend as PKernelFetchVerifiedBeforeUse
import ./proof/kernel_local/kernel_setup_runs.bend as PKernelSetupRuns
import ./proof/kernel_local/kernel_install_fetches.bend as PKernelInstallFetches
import ./proof/kernel_local/kernel_missing_spares_tools.bend as PKernelMissingSparesTools
import ./proof/kernel_local/kernel_missing_names_install.bend as PKernelMissingNamesInstall
import ./proof/kernel_local/kernel_lock_attempt_leaves_none.bend as PKernelLockAttemptLeavesNone
import ./proof/kernel_local/kernel_lock_sweep_removes_dead.bend as PKernelLockSweepRemovesDead
import ./proof/kernel_local/kernel_lock_sweep_keeps_live.bend as PKernelLockSweepKeepsLive
import ./proof/kernel_local/base.bend as LAKernelLocal
import ./proof/kernel_local/kernel_plan_exact.bend as PKernelPlanExact
import ./proof/kernel_local/kernel_lock_judge.bend as PKernelLockJudge
import ./proof/kernel_local/kernel_ffi_answers.bend as PKernelFfiAnswers
import ./proof/kernel_local/kernel_ffi_malformed.bend as PKernelFfiMalformed
import ./proof/kernel_local/kernel_ffi_example.bend as PKernelFfiExample
import ./proof/kernel_local/kernel_start_exact.bend as PKernelStartExact
import ./proof/kernel_local/kernel_answer_exact.bend as PKernelAnswerExact
import ./proof/kernel_local/kernel_ffi_malformed_exact.bend as PKernelFfiMalformedExact
import ./proof/kernel_local/kernel_terms_exact.bend as PKernelTermsExact
import ./proof/kernel_local/kernel_sweep_terms_exact.bend as PKernelSweepTermsExact
import ./proof/log/base.bend as LALog
import ./proof/log/log_reads_lines.bend as PLogReadsLines
import ./proof/log/log_ack_durable.bend as PLogAckDurable
import ./proof/log/log_only_commits.bend as PLogOnlyCommits
import ./proof/log/log_open_cuts_the_torn_tail.bend as PLogOpenCutsTheTornTail
import ./proof/log/log_open_keeps_the_complete_lines.bend as PLogOpenKeepsTheCompleteLines
import ./proof/log/log_open_refuses_odd_facts.bend as PLogOpenRefusesOddFacts
import ./proof/log/log_plan_runs_the_model.bend as PLogPlanRunsTheModel
import ./proof/log/log_plan_ack_durable.bend as PLogPlanAckDurable
import ./proof/log/log_plan_only_commits.bend as PLogPlanOnlyCommits
import ./proof/log/log_commit_plan.bend as PLogCommitPlan
import ./proof/log/log_open_plan.bend as PLogOpenPlan
import ./proof/log/log_ffi_answers_the_open.bend as PLogFfiAnswersTheOpen
import ./proof/log/log_ffi_reads_only_requests.bend as PLogFfiReadsOnlyRequests
import ./proof/log/log_ffi_reads_only_fitting_requests.bend as PLogFfiReadsOnlyFittingRequests
import ./proof/log/log_stepper_open.bend as PLogStepperOpen
import ./proof/log/log_stepper_open_reads_only_a_bool.bend as PLogStepperOpenReadsOnlyABool
import ./proof/log/log_stepper_open_refused_shuts.bend as PLogStepperOpenRefusedShuts
import ./proof/log/log_stepper_commit.bend as PLogStepperCommit
import ./proof/log/log_stepper_reads_only_commits.bend as PLogStepperReadsOnlyCommits
import ./proof/log/log_stepper_reads_only_fitting_commits.bend as PLogStepperReadsOnlyFittingCommits
import ./proof/log/log_stepper_refusal_keeps_the_state.bend as PLogStepperRefusalKeepsTheState
import ./proof/log/log_stepper_shut_refuses.bend as PLogStepperShutRefuses
import ./proof/log/log_fits_example.bend as PLogFitsExample
import ./proof/log/log_ffi_example.bend as PLogFfiExample
import ./proof/log/log_stepper_example.bend as PLogStepperExample
import ./proof/staging/base.bend as LAStaging
import ./proof/staging/publish_never_overwrites.bend as PPublishNeverOverwrites
import ./proof/staging/publish_moves.bend as PPublishMoves
import ./proof/staging/sweep_never_live.bend as PSweepNeverLive
import ./proof/staging/sweep_never_young.bend as PSweepNeverYoung
import ./proof/staging/sweep_stays_out.bend as PSweepStaysOut
import ./proof/staging/sweep_reaches_every_depth.bend as PSweepReachesEveryDepth
import ./proof/staging/list_one_location.bend as PListOneLocation
import ./proof/staging/list_import_lists_storage.bend as PListImportListsStorage
import ./proof/staging/list_import_keeps_others.bend as PListImportKeepsOthers
import ./proof/staging/judge_day_example.bend as PJudgeDayExample
import ./proof/staging/judge_exact.bend as PJudgeExact
import ./proof/staging/judge_refines.bend as PJudgeRefines
import ./proof/staging/meet_exact.bend as PMeetExact
import ./proof/staging/meet_minted_leftover.bend as PMeetMintedLeftover
import ./proof/staging/meet_minted_orphan.bend as PMeetMintedOrphan
import ./proof/staging/meet_names_example.bend as PMeetNamesExample
import ./proof/staging/publish_settle_refines.bend as PPublishSettleRefines
import ./proof/staging/publish_settles.bend as PPublishSettles
import ./proof/staging/staging_entry_answers.bend as PStagingEntryAnswers
import ./proof/staging/staging_entry_exact.bend as PStagingEntryExact
import ./proof/staging/staging_entry_example.bend as PStagingEntryExample
import ./proof/staging/staging_entry_malformed_example.bend as PStagingEntryMalformedExample
import ./proof/staging/sweep_never_live_real.bend as PSweepNeverLiveReal
import ./proof/staging/sweep_never_young_real.bend as PSweepNeverYoungReal
import ./proof/staging/sweep_stays_out_real.bend as PSweepStaysOutReal
import ./proof/staging/sweep_takes_stale_free_real.bend as PSweepTakesStaleFreeReal
import ./proof/listing/rows_are_entries.bend as PRowsAreEntries
import ./proof/listing/rows_each_once.bend as PRowsEachOnce
import ./proof/listing/rows_example.bend as PRowsExample
import ./proof/listing/rows_ignore_unread.bend as PRowsIgnoreUnread
import ./proof/listing/rows_newest_first.bend as PRowsNewestFirst
import ./proof/listing/rows_order_strict.bend as PRowsOrderStrict
import ./proof/listing/scan_exact.bend as PScanExact
import ./proof/listing/scan_example.bend as PScanExample
import ./proof/listing/scan_import_keeps_others.bend as PScanImportKeepsOthers
import ./proof/listing/scan_import_lists_storage.bend as PScanImportListsStorage
import ./proof/listing/scan_legacy_named.bend as PScanLegacyNamed
import ./proof/listing/scan_one_location.bend as PScanOneLocation
import ./proof/catalog_union/base.bend as LACatalogUnion
import ./proof/catalog_union/union_hides_nothing.bend as PUnionHidesNothing
import ./proof/catalog_union/union_lists_each_model_once.bend as PUnionListsEachModelOnce
import ./proof/catalog_union/union_bundled_only.bend as PUnionBundledOnly
import ./proof/catalog_union/union_compiled_only.bend as PUnionCompiledOnly
import ./proof/catalog_union/union_both_keeps_bundled.bend as PUnionBothKeepsBundled
import ./proof/catalog_union/union_both_fills_from_compiled.bend as PUnionBothFillsFromCompiled
import ./proof/catalog_union/union_both_other_api.bend as PUnionBothOtherApi
import ./proof/catalog_union/union_fields_example.bend as PUnionFieldsExample
import ./proof/catalog_union/union_fast.bend as PUnionFast
import ./proof/catalog_union/union_order_free.bend as PUnionOrderFree
import ./proof/catalog_union/catalog_union_ffi_request_round_trip.bend as PCatalogUnionFfiRequestRoundTrip
import ./proof/catalog_union/catalog_union_ffi_answers.bend as PCatalogUnionFfiAnswers
import ./proof/catalog_union/catalog_union_ffi_rejects_malformed.bend as PCatalogUnionFfiRejectsMalformed
import ./proof/catalog_union/catalog_union_ffi_rejects_left_over.bend as PCatalogUnionFfiRejectsLeftOver
import ./proof/cron/base/bool.bend as LACronBool
import ./proof/cron/base/cron.bend as LACronCron
import ./proof/cron/base/list.bend as LACronList
import ./proof/cron/base/logic.bend as LACronLogic
import ./proof/cron/base/nat.bend as LACronNat
import ./proof/cron/cron_fires_once.bend as PCronFiresOnce
import ./proof/cron/cron_once_finished_after_end.bend as PCronOnceFinishedAfterEnd
import ./proof/cron/cron_never_drops.bend as PCronNeverDrops
import ./proof/cron/cron_claim_owned.bend as PCronClaimOwned
import ./proof/cron/cron_backoff_bounded.bend as PCronBackoffBounded
import ./proof/supervise/base.bend as LASupervise
import ./proof/supervise/restart_gives_up.bend as PRestartGivesUp
import ./proof/supervise/restart_decide_window.bend as PRestartDecideWindow
import ./proof/supervise/restart_decide_verdict.bend as PRestartDecideVerdict
import ./proof/supervise/restart_wire_req.bend as PRestartWireReq
import ./proof/supervise/restart_wire_reply_relaunch.bend as PRestartWireReplyRelaunch
import ./proof/supervise/restart_wire_reply_give_up.bend as PRestartWireReplyGiveUp
import ./proof/supervise/restart_ffi_decides.bend as PRestartFfiDecides
import ./proof/supervise/restart_ffi_malformed.bend as PRestartFfiMalformed
import ./proof/supervise/restart_ffi_left_over.bend as PRestartFfiLeftOver
import ./proof/supervise/timeouts_ordered.bend as PTimeoutsOrdered
import ./proof/revive/revive_after_refresh.bend as PReviveAfterRefresh
import ./proof/timeouts/base.bend as LATimeouts
import ./proof/timeouts/timeouts_ffi_answers.bend as PTimeoutsFfiAnswers
import ./proof/timeouts/timeouts_ffi_reads.bend as PTimeoutsFfiReads
import ./proof/timeouts/timeouts_ffi_malformed_exact.bend as PTimeoutsFfiMalformedExact
import ./proof/timeouts/timeouts_ffi_example.bend as PTimeoutsFfiExample
import ./proof/timeouts/timeouts_values_are_model.bend as PTimeoutsValuesAreModel
import ./proof/revive/base.bend as LARevive
import ./proof/revive/revive_ffi_answers.bend as PReviveFfiAnswers
import ./proof/revive/revive_ffi_reads.bend as PReviveFfiReads
import ./proof/revive/revive_ffi_malformed_exact.bend as PReviveFfiMalformedExact
import ./proof/revive/revive_ffi_example.bend as PReviveFfiExample
import ./proof/revive/revive_veto_ages_as_model.bend as PReviveVetoAgesAsModel
import ./proof/revive/revive_ffi_ages_as_model.bend as PReviveFfiAgesAsModel
import ./proof/orphan/base.bend as LAOrphan
import ./proof/orphan/orphan_never_aborts_resumable.bend as POrphanNeverAbortsResumable
import ./proof/orphan/orphan_idle_exit_due.bend as POrphanIdleExitDue
import ./proof/orphan/orphan_work_exit_due.bend as POrphanWorkExitDue
import ./proof/orphan/orphan_capped_window_never_expires.bend as POrphanCappedWindowNeverExpires
import ./proof/orphan/orphan_exit_by_work.bend as POrphanExitByWork
import ./proof/orphan/orphan_wire_req_window.bend as POrphanWireReqWindow
import ./proof/orphan/orphan_wire_req_no_window.bend as POrphanWireReqNoWindow
import ./proof/orphan/orphan_wire_reply.bend as POrphanWireReply
import ./proof/orphan/orphan_ffi_decides.bend as POrphanFfiDecides
import ./proof/orphan/orphan_ffi_malformed.bend as POrphanFfiMalformed
import ./proof/orphan/orphan_ffi_left_over.bend as POrphanFfiLeftOver
import ./proof/launcher/idle_shutdown_never_aborts.bend as PIdleShutdownNeverAborts
import ./proof/launcher/adopt_same_build.bend as PAdoptSameBuild
import ./proof/launcher/base.bend as LALauncher
import ./proof/launcher/launcher_ffi_answers.bend as PLauncherFfiAnswers
import ./proof/launcher/launcher_ffi_malformed.bend as PLauncherFfiMalformed
import ./proof/launcher/launcher_ffi_example.bend as PLauncherFfiExample
import ./proof/launcher/launcher_stop_counts_runs.bend as PLauncherStopCountsRuns
import ./proof/launcher/launcher_step_exact.bend as PLauncherStepExact
import ./proof/launcher/launcher_closed_gate_waits_example.bend as PLauncherClosedGateWaitsExample
import ./proof/launcher/launcher_ffi_malformed_exact.bend as PLauncherFfiMalformedExact
import ./proof/launcher/launcher_adoption_exact.bend as PLauncherAdoptionExact
import ./proof/replace/base.bend as LAReplace
import ./proof/replace/replace_never_downgrades.bend as PReplaceNeverDowngrades
import ./proof/replace/replacement_terminates.bend as PReplacementTerminates
import ./proof/replace/background_never_replaces.bend as PBackgroundNeverReplaces
import ./proof/replace/replace_rank_reads_semver.bend as PReplaceRankReadsSemver
import ./proof/replace/replace_rank_example.bend as PReplaceRankExample
import ./proof/replace/replace_rank_past_range_example.bend as PReplaceRankPastRangeExample
import ./proof/replace/replace_relation_exact.bend as PReplaceRelationExact
import ./proof/replace/replace_verdict_exact.bend as PReplaceVerdictExact
import ./proof/replace/replace_ping_pong_example.bend as PReplacePingPongExample
import ./proof/replace/replace_rank_cut.bend as PReplaceRankCut
import ./proof/replace/replace_ffi_relation.bend as PReplaceFfiRelation
import ./proof/replace/replace_ffi_verdict.bend as PReplaceFfiVerdict
import ./proof/replace/replace_ffi_example.bend as PReplaceFfiExample
import ./proof/notice/base.bend as LANotice
import ./proof/notice/notice_shown_once.bend as PNoticeShownOnce
import ./proof/notice/notice_per_restore.bend as PNoticePerRestore
import ./proof/notice/notice_rule_history.bend as PNoticeRuleHistory
import ./proof/notice/notice_real_shown_once.bend as PNoticeRealShownOnce
import ./proof/notice/notice_real_record_keeps.bend as PNoticeRealRecordKeeps
import ./proof/notice/notice_real_apart.bend as PNoticeRealApart
import ./proof/notice/notice_real_other_shows.bend as PNoticeRealOtherShows
import ./proof/notice/notice_real_custom_shows.bend as PNoticeRealCustomShows
import ./proof/notice/notice_real_refines.bend as PNoticeRealRefines
import ./proof/notice/notice_real_once.bend as PNoticeRealOnce
import ./proof/notice/notice_real_per_restore.bend as PNoticeRealPerRestore
import ./proof/notice/notice_once_exact.bend as PNoticeOnceExact
import ./proof/notice/notice_ffi_open.bend as PNoticeFfiOpen
import ./proof/notice/notice_ffi_open_refused.bend as PNoticeFfiOpenRefused
import ./proof/notice/notice_ffi_shut.bend as PNoticeFfiShut
import ./proof/notice/notice_ffi_step.bend as PNoticeFfiStep
import ./proof/notice/notice_ffi_history.bend as PNoticeFfiHistory
import ./proof/notice/notice_ffi_exact.bend as PNoticeFfiExact
import ./proof/notice/notice_ffi_malformed.bend as PNoticeFfiMalformed
import ./proof/notice/notice_ffi_fits_witness.bend as PNoticeFfiFitsWitness
import ./proof/notice/notice_ffi_spell_example.bend as PNoticeFfiSpellExample
import ./proof/notice/notice_ffi_wire_example.bend as PNoticeFfiWireExample
import ./proof/notice/notice_ffi_malformed_witness.bend as PNoticeFfiMalformedWitness
import ./proof/gateway_width/base.bend as LAGatewayWidth
import ./proof/gateway_width/table_aligned.bend as PTableAligned
import ./proof/gateway_width/ascii_unchanged.bend as PAsciiUnchanged
import ./proof/gateway_width/layout_widths.bend as PLayoutWidths
import ./proof/gateway_width/layout_pads.bend as PLayoutPads
import ./proof/gateway_width/gateway_width_ffi_request_round_trip.bend as PGatewayWidthFfiRequestRoundTrip
import ./proof/gateway_width/gateway_width_ffi_answers.bend as PGatewayWidthFfiAnswers
import ./proof/gateway_width/gateway_width_ffi_rejects_malformed.bend as PGatewayWidthFfiRejectsMalformed
import ./proof/gateway_width/gateway_width_ffi_rejects_left_over.bend as PGatewayWidthFfiRejectsLeftOver
import ./proof/tui_color/base.bend as LATuiColor
import ./proof/tui_color/tui_effort_ramp_length.bend as PTuiEffortRampLength
import ./proof/tui_color/tui_effort_ramp_ordered.bend as PTuiEffortRampOrdered
import ./proof/tui_color/tui_effort_ramp_distinct.bend as PTuiEffortRampDistinct
import ./proof/tui_color/tui_effort_shipped_distinct.bend as PTuiEffortShippedDistinct
import ./proof/tui_color/tui_usage_bands_ascend.bend as PTuiUsageBandsAscend
import ./proof/tui_color/tui_usage_band_monotone.bend as PTuiUsageBandMonotone
import ./proof/tui_color/tui_usage_band_fraction.bend as PTuiUsageBandFraction
import ./proof/tui_color/tui_usage_band_full.bend as PTuiUsageBandFull
import ./proof/tui_color/tui_roles_shipped.bend as PTuiRolesShipped
import ./proof/fsmode/base.bend as LAFsmode
import ./proof/fsmode/socket_dir_owned.bend as PSocketDirOwned
import ./proof/fsmode/socket_dir_progress.bend as PSocketDirProgress
import ./proof/fsmode/fsmode_ffi_answers.bend as PFsmodeFfiAnswers
import ./proof/fsmode/fsmode_ffi_malformed.bend as PFsmodeFfiMalformed
import ./proof/fsmode/fsmode_ffi_example.bend as PFsmodeFfiExample
import ./proof/fsmode/fsmode_ffi_malformed_exact.bend as PFsmodeFfiMalformedExact
import ./proof/fsmode/fsmode_socket_dir_exact.bend as PFsmodeSocketDirExact
import ./proof/fsmode/fsmode_safe_exact.bend as PFsmodeSafeExact
import ./proof/fsmode/fsmode_modes_exact.bend as PFsmodeModesExact
import ./proof/fsmode/socket_dir_created.bend as PSocketDirCreated
import ./proof/fsmode/socket_dir_created_used.bend as PSocketDirCreatedUsed
import ./proof/fsmode/peer_same_uid.bend as PPeerSameUid
import ./proof/fsmode/peer_own_accepted.bend as PPeerOwnAccepted
import ./proof/fsmode/private_on_create.bend as PPrivateOnCreate
import ./proof/fsmode/cwd_is_explicit.bend as PCwdIsExplicit
import ./proof/fsmode/cwd_none_refused.bend as PCwdNoneRefused
import ./proof/fsmode/cwd_gone_refused.bend as PCwdGoneRefused
import ./proof/fsmode/cwd_file_refused.bend as PCwdFileRefused
import ./proof/fsmode/cwd_dir_opens.bend as PCwdDirOpens
import ./proof/path_policy/base.bend as LAPathPolicy
import ./proof/path_policy/path_real_has_no_link.bend as PPathRealHasNoLink
import ./proof/path_policy/path_secret_wins.bend as PPathSecretWins
import ./proof/path_policy/path_inside_is_safe.bend as PPathInsideIsSafe
import ./proof/path_policy/path_ancestor_guarded.bend as PPathAncestorGuarded
import ./proof/path_policy/path_judge_class.bend as PPathJudgeClass
import ./proof/path_policy/path_judge_holds.bend as PPathJudgeHolds
import ./proof/path_policy/gate_write_auto_never_secret.bend as PGateWriteAutoNeverSecret
import ./proof/path_policy/gate_secret_read_needs_yes.bend as PGateSecretReadNeedsYes
import ./proof/path_policy/gate_yes_runs.bend as PGateYesRuns
import ./proof/path_policy/secrets_need_yes.bend as PSecretsNeedYes
import ./proof/path_policy/path_policy_ffi_request_round_trip.bend as PPathPolicyFfiRequestRoundTrip
import ./proof/path_policy/path_policy_ffi_answers.bend as PPathPolicyFfiAnswers
import ./proof/path_policy/path_policy_ffi_rejects_malformed.bend as PPathPolicyFfiRejectsMalformed
import ./proof/path_policy/path_policy_ffi_rejects_left_over.bend as PPathPolicyFfiRejectsLeftOver
import ./proof/child_env/base.bend as LAChildEnv
import ./proof/child_env/env_drops_credentials.bend as PEnvDropsCredentials
import ./proof/child_env/env_kernel_keeps_only_listed.bend as PEnvKernelKeepsOnlyListed
import ./proof/child_env/env_keeps_the_rest.bend as PEnvKeepsTheRest
import ./proof/child_env/env_keeps_listed.bend as PEnvKeepsListed
import ./proof/child_env/env_child_from_merge.bend as PEnvChildFromMerge
import ./proof/child_env/env_overlay_in_merge.bend as PEnvOverlayInMerge
import ./proof/child_env/env_base_in_merge.bend as PEnvBaseInMerge
import ./proof/child_env/env_merge_named_from_overlay.bend as PEnvMergeNamedFromOverlay
import ./proof/child_env/env_merge_from_inputs.bend as PEnvMergeFromInputs
import ./proof/child_env/env_cred_example.bend as PEnvCredExample
import ./proof/child_env/env_not_cred_example.bend as PEnvNotCredExample
import ./proof/child_env/env_registry_example.bend as PEnvRegistryExample
import ./proof/child_env/env_step_example.bend as PEnvStepExample
import ./proof/child_env/env_kernel_example.bend as PEnvKernelExample
import ./proof/child_env/env_ffi_round_trip.bend as PEnvFfiRoundTrip
import ./proof/child_env/env_ffi_is_child.bend as PEnvFfiIsChild
import ./proof/child_env/env_ffi_malformed.bend as PEnvFfiMalformed
import ./proof/child_env/env_ffi_left_over.bend as PEnvFfiLeftOver
import ./proof/child_env/env_req_fits_example.bend as PEnvReqFitsExample
import ./proof/runners/base.bend as LARunners
import ./proof/runners/gate_covers_every_runner.bend as PGateCoversEveryRunner
import ./proof/runners/ipython_gated_each_call.bend as PIpythonGatedEachCall
import ./proof/runners/cell_runs_only_within_or_approved.bend as PCellRunsOnlyWithinOrApproved
import ./proof/runners/cell_within_runs_unasked.bend as PCellWithinRunsUnasked
import ./proof/runners/cell_approved_runs.bend as PCellApprovedRuns
import ./proof/runners/cell_no_yes_stops.bend as PCellNoYesStops
import ./proof/runners/cell_exec_asks.bend as PCellExecAsks
import ./proof/approvals/base.bend as LAApprovals
import ./proof/approvals/child_answered_by_root.bend as PChildAnsweredByRoot
import ./proof/approvals/nearest_answer_wins.bend as PNearestAnswerWins
import ./proof/approvals/unanswered_only_when_quiet.bend as PUnansweredOnlyWhenQuiet
import ./proof/approvals/quiet_is_unanswered.bend as PQuietIsUnanswered
import ./proof/approvals/gateway_never_waits.bend as PGatewayNeverWaits
import ./proof/approvals/left_to_the_gateway.bend as PLeftToTheGateway
import ./proof/approvals/gateway_rules_a_subagent.bend as PGatewayRulesASubagent
import ./proof/wire/base.bend as LAWire
import ./proof/wire/wire_nat_exact.bend as PWireNatExact
import ./proof/wire/wire_nat_decoded_fits.bend as PWireNatDecodedFits
import ./proof/wire/wire_nat_too_long.bend as PWireNatTooLong
import ./proof/wire/wire_too_long_exists.bend as PWireTooLongExists
import ./proof/wire/wire_nat_not_err.bend as PWireNatNotErr
import ./proof/wire/wire_nat_example.bend as PWireNatExample
import ./proof/wire/wire_nat_zero_example.bend as PWireNatZeroExample
import ./proof/wire/wire_nat_leading_zero_example.bend as PWireNatLeadingZeroExample
import ./proof/wire/wire_nat_unterminated_example.bend as PWireNatUnterminatedExample
import ./proof/wire/wire_digits_spells.bend as PWireDigitsSpells
import ./proof/wire/wire_u32_round_trip.bend as PWireU32RoundTrip
import ./proof/wire/wire_u32_exact.bend as PWireU32Exact
import ./proof/wire/wire_u32_example.bend as PWireU32Example
import ./proof/wire/wire_bool_round_trip.bend as PWireBoolRoundTrip
import ./proof/wire/wire_bool_exact.bend as PWireBoolExact
import ./proof/wire/wire_bool_not_err.bend as PWireBoolNotErr
import ./proof/wire/wire_bool_example.bend as PWireBoolExample
import ./proof/wire/wire_str_exact.bend as PWireStrExact
import ./proof/wire/wire_str_example.bend as PWireStrExample
import ./proof/wire/wire_list_exact.bend as PWireListExact
import ./proof/wire/wire_list_example.bend as PWireListExample
import ./proof/wire/wire_err_example.bend as PWireErrExample
import ./proof/wire/wire_end_exact.bend as PWireEndExact
import ./proof/facts/base.bend as LAFacts
import ./proof/facts/core_facts_round_trip.bend as PCoreFactsRoundTrip
import ./proof/facts/core_facts_level.bend as PCoreFactsLevel
import ./proof/facts/core_facts_room.bend as PCoreFactsRoom
import ./proof/facts/core_facts_adjust.bend as PCoreFactsAdjust
import ./proof/facts/core_facts_google.bend as PCoreFactsGoogle
import ./proof/facts/core_facts_aux.bend as PCoreFactsAux
import ./proof/facts/core_facts_malformed.bend as PCoreFactsMalformed
import ./proof/facts/core_facts_left_over.bend as PCoreFactsLeftOver
import ./proof/facts/core_facts_req_example.bend as PCoreFactsReqExample
import ./proof/facts/core_facts_reply_example.bend as PCoreFactsReplyExample
import ./proof/facts/core_facts_malformed_example.bend as PCoreFactsMalformedExample
import ./proof/facts/facts_adaptive_compat_first.bend as PFactsAdaptiveCompatFirst
import ./proof/facts/facts_adaptive_rulebook_second.bend as PFactsAdaptiveRulebookSecond
import ./proof/facts/facts_google_budget_at_most_high.bend as PFactsGoogleBudgetAtMostHigh
import ./proof/facts/facts_google_budget_at_least_minimal.bend as PFactsGoogleBudgetAtLeastMinimal
import ./proof/facts/facts_google_rule_is_the_table.bend as PFactsGoogleRuleIsTheTable
import ./proof/facts/facts_fit_budget_under_ceiling.bend as PFactsFitBudgetUnderCeiling
import ./proof/facts/facts_fit_ceiling_under_model.bend as PFactsFitCeilingUnderModel
import ./proof/facts/facts_room_leaves_the_answer.bend as PFactsRoomLeavesTheAnswer
import ./proof/facts/facts_aux_cap_answer_room.bend as PFactsAuxCapAnswerRoom
import ./proof/facts/facts_google_unordered_refused.bend as PFactsGoogleUnorderedRefused
import ./proof/facts/facts_google_ordered_tokens.bend as PFactsGoogleOrderedTokens
import ./proof/facts/facts_google_budget_held.bend as PFactsGoogleBudgetHeld
import ./proof/facts/facts_google_free_user.bend as PFactsGoogleFreeUser
import ./proof/facts/facts_google_free_dynamic.bend as PFactsGoogleFreeDynamic
import ./proof/facts/facts_budget_levels.bend as PFactsBudgetLevels
import ./proof/facts/facts_budget_user_first.bend as PFactsBudgetUserFirst
import ./proof/facts/facts_budget_default.bend as PFactsBudgetDefault
import ./proof/facts/facts_fit_exact_caller.bend as PFactsFitExactCaller
import ./proof/facts/facts_fit_exact_model.bend as PFactsFitExactModel
import ./proof/facts/facts_fit_saturated_caller.bend as PFactsFitSaturatedCaller
import ./proof/facts/facts_fit_saturated_budget.bend as PFactsFitSaturatedBudget
import ./proof/facts/facts_aux_cap_within.bend as PFactsAuxCapWithin
import ./proof/facts/facts_bedrock_effort_oracle.bend as PFactsBedrockEffortOracle
import ./proof/facts/facts_bedrock_budget_oracle.bend as PFactsBedrockBudgetOracle
import ./proof/facts/facts_tier_price_model_row_first.bend as PFactsTierPriceModelRowFirst
import ./proof/facts/facts_tier_price_no_row_base.bend as PFactsTierPriceNoRowBase
import ./proof/facts/facts_tier_price_openai_oracle.bend as PFactsTierPriceOpenaiOracle
import ./proof/facts/facts_tier_price_codex_oracle.bend as PFactsTierPriceCodexOracle
import ./proof/facts/facts_cache_write_1h_own_rate.bend as PFactsCacheWrite1hOwnRate
import ./proof/facts/facts_flag_exact.bend as PFactsFlagExact
import ./proof/facts/facts_effort_exact.bend as PFactsEffortExact
import ./proof/facts/facts_price_exact.bend as PFactsPriceExact
import ./proof/facts/facts_customs_at_exact.bend as PFactsCustomsAtExact
import ./proof/facts/facts_aux_exact.bend as PFactsAuxExact
import ./proof/model_facts/base.bend as LAModelFacts
import ./proof/model_facts/model_facts_ffi_flag.bend as PModelFactsFfiFlag
import ./proof/model_facts/model_facts_ffi_adaptive.bend as PModelFactsFfiAdaptive
import ./proof/model_facts/model_facts_ffi_effort.bend as PModelFactsFfiEffort
import ./proof/model_facts/model_facts_ffi_price.bend as PModelFactsFfiPrice
import ./proof/model_facts/model_facts_ffi_malformed_exact.bend as PModelFactsFfiMalformedExact
import ./proof/model_facts/model_facts_ffi_example.bend as PModelFactsFfiExample
import ./proof/retry/base.bend as LARetry
import ./proof/retry/retry_never_parked.bend as PRetryNeverParked
import ./proof/retry/retry_never_limit.bend as PRetryNeverLimit
import ./proof/retry/retry_never_client_error.bend as PRetryNeverClientError
import ./proof/retry/retry_only_retryable.bend as PRetryOnlyRetryable
import ./proof/retry/retry_status_first.bend as PRetryStatusFirst
import ./proof/retry/retry_kind_before_text.bend as PRetryKindBeforeText
import ./proof/retry/retry_server_errors.bend as PRetryServerErrors
import ./proof/retry/retry_classifier_exact.bend as PRetryClassifierExact
import ./proof/retry/retry_classifier_example.bend as PRetryClassifierExample
import ./proof/retry/retry_after_respected.bend as PRetryAfterRespected
import ./proof/retry/retry_refuses_past_cap.bend as PRetryRefusesPastCap
import ./proof/retry/retry_wait_plain.bend as PRetryWaitPlain
import ./proof/retry/retry_wait_uncapped.bend as PRetryWaitUncapped
import ./proof/retry/retry_wait_within_cap.bend as PRetryWaitWithinCap
import ./proof/retry/retry_wait_saturation_exact.bend as PRetryWaitSaturationExact
import ./proof/retry/retry_step_exact.bend as PRetryStepExact
import ./proof/retry/retry_step_example.bend as PRetryStepExample
import ./proof/retry/retry_jitter_exact.bend as PRetryJitterExact
import ./proof/retry/retry_jitter_zero_step.bend as PRetryJitterZeroStep
import ./proof/retry/retry_wait_composes.bend as PRetryWaitComposes
import ./proof/retry/failover_visits_once.bend as PFailoverVisitsOnce
import ./proof/retry/failover_never_twice_in_a_row.bend as PFailoverNeverTwiceInARow
import ./proof/retry/failover_return_waits.bend as PFailoverReturnWaits
import ./proof/retry/failover_delay_capped.bend as PFailoverDelayCapped
import ./proof/retry/failover_bounded.bend as PFailoverBounded
import ./proof/retry/failover_exact.bend as PFailoverExact
import ./proof/retry/failover_example.bend as PFailoverExample
import ./proof/retry/failover_budget_example.bend as PFailoverBudgetExample
import ./proof/retry/failover_wait_saturation_exact.bend as PFailoverWaitSaturationExact
import ./proof/retry/failover_base_saturation_exact.bend as PFailoverBaseSaturationExact
import ./proof/retry/deferred_pays_once.bend as PDeferredPaysOnce
import ./proof/retry/deferred_bounded_in_time.bend as PDeferredBoundedInTime
import ./proof/retry/deferred_failed_poll_repolls.bend as PDeferredFailedPollRepolls
import ./proof/retry/stall_retry_extends.bend as PStallRetryExtends
import ./proof/retry/stall_retry_doubles.bend as PStallRetryDoubles
import ./proof/retry/stall_detection_bounded.bend as PStallDetectionBounded
import ./proof/retry/stall_silent_ends_at_deadline.bend as PStallSilentEndsAtDeadline
import ./proof/retry/retry_ffi_request_round_trip.bend as PRetryFfiRequestRoundTrip
import ./proof/retry/retry_ffi_request_exact.bend as PRetryFfiRequestExact
import ./proof/retry/retry_ffi_classify.bend as PRetryFfiClassify
import ./proof/retry/retry_ffi_wait.bend as PRetryFfiWait
import ./proof/retry/retry_ffi_failover.bend as PRetryFfiFailover
import ./proof/retry/retry_ffi_stall.bend as PRetryFfiStall
import ./proof/retry/retry_ffi_malformed.bend as PRetryFfiMalformed
import ./proof/retry/retry_ffi_trailing.bend as PRetryFfiTrailing
import ./proof/retry/retry_ffi_fits_exists.bend as PRetryFfiFitsExists
import ./proof/retry/retry_ffi_example.bend as PRetryFfiExample
import ./proof/dash/base.bend as LADash
import ./proof/dash/dash_frame_runs_only_current.bend as PDashFrameRunsOnlyCurrent
import ./proof/dash/dash_current_frame_runs.bend as PDashCurrentFrameRuns
import ./proof/dash/dash_open_pairs_only_current.bend as PDashOpenPairsOnlyCurrent
import ./proof/dash/dash_current_open_pairs.bend as PDashCurrentOpenPairs
import ./proof/dash/dash_paired_holds_token.bend as PDashPairedHoldsToken
import ./proof/dash/dash_closed_runs_nothing.bend as PDashClosedRunsNothing
import ./proof/dash/dash_rejected_runs_nothing.bend as PDashRejectedRunsNothing
import ./proof/dash/dash_rotation_ends_connections.bend as PDashRotationEndsConnections
import ./proof/dash/dash_rotation_rejects_old_tokens.bend as PDashRotationRejectsOldTokens
import ./proof/dash/dash_token_spec.bend as PDashTokenSpec
import ./proof/dash/dash_stored_spec.bend as PDashStoredSpec
import ./proof/dash/dash_gate_spec.bend as PDashGateSpec
import ./proof/dash/dash_frame_spec.bend as PDashFrameSpec
import ./proof/dash/dash_keep_spec.bend as PDashKeepSpec
import ./proof/dash/dash_gate_is_model.bend as PDashGateIsModel
import ./proof/dash/dash_frame_is_model.bend as PDashFrameIsModel
import ./proof/dash/dash_token_example.bend as PDashTokenExample
import ./proof/dash/dash_entry_answers.bend as PDashEntryAnswers
import ./proof/dash/dash_entry_reads.bend as PDashEntryReads
import ./proof/dash/dash_entry_exact.bend as PDashEntryExact
import ./proof/dash/dash_entry_refuses.bend as PDashEntryRefuses
import ./proof/dash/dash_entry_example.bend as PDashEntryExample
import ./proof/dash_policy/base.bend as LADashPolicy
import ./proof/dash_policy/dash_policy_spec.bend as PDashPolicySpec
import ./proof/dash_policy/dash_policy_owned_refused.bend as PDashPolicyOwnedRefused
import ./proof/dash_policy/dash_policy_example.bend as PDashPolicyExample
import ./proof/dash_policy/dash_policy_entry_reads.bend as PDashPolicyEntryReads
import ./proof/dash_policy/dash_policy_entry_answers.bend as PDashPolicyEntryAnswers
import ./proof/dash_policy/dash_policy_entry_exact.bend as PDashPolicyEntryExact
import ./proof/dash_policy/dash_policy_entry_refuses.bend as PDashPolicyEntryRefuses
import ./proof/dash_policy/dash_policy_entry_example.bend as PDashPolicyEntryExample
import ./proof/dash_access/base.bend as LADashAccess
import ./proof/dash_access/dash_access_host_spec.bend as PDashAccessHostSpec
import ./proof/dash_access/dash_access_host_long_port.bend as PDashAccessHostLongPort
import ./proof/dash_access/dash_access_origin_spec.bend as PDashAccessOriginSpec
import ./proof/dash_access/dash_access_host_01_example.bend as PDashAccessHost01Example
import ./proof/dash_access/dash_access_host_02_example.bend as PDashAccessHost02Example
import ./proof/dash_access/dash_access_host_03_example.bend as PDashAccessHost03Example
import ./proof/dash_access/dash_access_host_04_example.bend as PDashAccessHost04Example
import ./proof/dash_access/dash_access_host_05_example.bend as PDashAccessHost05Example
import ./proof/dash_access/dash_access_host_06_example.bend as PDashAccessHost06Example
import ./proof/dash_access/dash_access_host_07_example.bend as PDashAccessHost07Example
import ./proof/dash_access/dash_access_host_08_example.bend as PDashAccessHost08Example
import ./proof/dash_access/dash_access_host_09_example.bend as PDashAccessHost09Example
import ./proof/dash_access/dash_access_host_10_example.bend as PDashAccessHost10Example
import ./proof/dash_access/dash_access_host_11_example.bend as PDashAccessHost11Example
import ./proof/dash_access/dash_access_host_12_example.bend as PDashAccessHost12Example
import ./proof/dash_access/dash_access_host_13_example.bend as PDashAccessHost13Example
import ./proof/dash_access/dash_access_host_14_example.bend as PDashAccessHost14Example
import ./proof/dash_access/dash_access_host_15_example.bend as PDashAccessHost15Example
import ./proof/dash_access/dash_access_host_16_example.bend as PDashAccessHost16Example
import ./proof/dash_access/dash_access_host_17_example.bend as PDashAccessHost17Example
import ./proof/dash_access/dash_access_host_18_example.bend as PDashAccessHost18Example
import ./proof/dash_access/dash_access_host_19_example.bend as PDashAccessHost19Example
import ./proof/dash_access/dash_access_host_20_example.bend as PDashAccessHost20Example
import ./proof/dash_access/dash_access_host_21_example.bend as PDashAccessHost21Example
import ./proof/dash_access/dash_access_host_22_example.bend as PDashAccessHost22Example
import ./proof/dash_access/dash_access_host_23_example.bend as PDashAccessHost23Example
import ./proof/dash_access/dash_access_host_24_example.bend as PDashAccessHost24Example
import ./proof/dash_access/dash_access_host_25_example.bend as PDashAccessHost25Example
import ./proof/dash_access/dash_access_origin_example.bend as PDashAccessOriginExample
import ./proof/dash_access/dash_access_entry_reads.bend as PDashAccessEntryReads
import ./proof/dash_access/dash_access_entry_answers.bend as PDashAccessEntryAnswers
import ./proof/dash_access/dash_access_entry_exact.bend as PDashAccessEntryExact
import ./proof/dash_access/dash_access_entry_refuses.bend as PDashAccessEntryRefuses
import ./proof/dash_access/dash_access_entry_example.bend as PDashAccessEntryExample
import ./proof/gateway_backoff/gateway_backoff_spec.bend as PGatewayBackoffSpec
import ./proof/gateway_backoff/gateway_backoff_bounded.bend as PGatewayBackoffBounded
import ./proof/gateway_backoff/gateway_backoff_example.bend as PGatewayBackoffExample
import ./proof/gateway_backoff/gateway_backoff_entry_reads.bend as PGatewayBackoffEntryReads
import ./proof/gateway_backoff/gateway_backoff_entry_answers.bend as PGatewayBackoffEntryAnswers
import ./proof/gateway_backoff/gateway_backoff_entry_exact.bend as PGatewayBackoffEntryExact
import ./proof/gateway_backoff/gateway_backoff_entry_refuses.bend as PGatewayBackoffEntryRefuses
import ./proof/gateway_backoff/gateway_backoff_entry_example.bend as PGatewayBackoffEntryExample
import ./proof/gateway_backoff/gateway_backoff_entry_capped.bend as PGatewayBackoffEntryCapped
import ./proof/slash_suggest/base.bend as LASlashSuggest
import ./proof/slash_suggest/slash_suggest_distance.bend as PSlashSuggestDistance
import ./proof/slash_suggest/slash_suggest_spec.bend as PSlashSuggestSpec
import ./proof/slash_suggest/slash_suggest_example.bend as PSlashSuggestExample
import ./proof/slash_suggest/slash_suggest_distance_example.bend as PSlashSuggestDistanceExample
import ./proof/slash_suggest/slash_suggest_entry_answers.bend as PSlashSuggestEntryAnswers
import ./proof/slash_suggest/slash_suggest_entry_reads.bend as PSlashSuggestEntryReads
import ./proof/slash_suggest/slash_suggest_entry_exact.bend as PSlashSuggestEntryExact
import ./proof/slash_suggest/slash_suggest_entry_refuses.bend as PSlashSuggestEntryRefuses
import ./proof/slash_suggest/slash_suggest_entry_example.bend as PSlashSuggestEntryExample
import ./proof/gateway_commands/base.bend as LAGatewayCommands
import ./proof/gateway_commands/gateway_commands_entry_answers.bend as PGatewayCommandsEntryAnswers
import ./proof/gateway_commands/gateway_commands_entry_exact.bend as PGatewayCommandsEntryExact
import ./proof/gateway_commands/gateway_commands_entry_example.bend as PGatewayCommandsEntryExample
import ./proof/gateway_commands/gateway_commands_entry_reads.bend as PGatewayCommandsEntryReads
import ./proof/gateway_commands/gateway_commands_entry_refuses.bend as PGatewayCommandsEntryRefuses
import ./proof/gateway_commands/gateway_commands_example.bend as PGatewayCommandsExample
import ./proof/gateway_commands/gateway_commands_spec.bend as PGatewayCommandsSpec
import ./proof/gateway_answer/base.bend as LAGatewayAnswer
import ./proof/gateway_answer/gateway_answer_spec.bend as PGatewayAnswerSpec
import ./proof/gateway_answer/gateway_answer_example.bend as PGatewayAnswerExample
import ./proof/gateway_answer/gateway_answer_entry_reads.bend as PGatewayAnswerEntryReads
import ./proof/gateway_answer/gateway_answer_entry_answers.bend as PGatewayAnswerEntryAnswers
import ./proof/gateway_answer/gateway_answer_entry_exact.bend as PGatewayAnswerEntryExact
import ./proof/gateway_answer/gateway_answer_entry_refuses.bend as PGatewayAnswerEntryRefuses
import ./proof/gateway_answer/gateway_answer_entry_example.bend as PGatewayAnswerEntryExample
import ./proof/doc_commit/base.bend as LADocCommit
import ./proof/doc_commit/edit_reports_what_landed.bend as PEditReportsWhatLanded
import ./proof/doc_commit/edit_all_or_nothing_on_conflict.bend as PEditAllOrNothingOnConflict
import ./proof/doc_commit/edit_lands_every_file.bend as PEditLandsEveryFile
import ./proof/doc_commit/write_never_loses_unseen.bend as PWriteNeverLosesUnseen
import ./proof/doc_commit/write_writes_seen.bend as PWriteWritesSeen
import ./proof/doc_commit/move_never_overwrites.bend as PMoveNeverOverwrites
import ./proof/doc_commit/move_moves.bend as PMoveMoves
import ./proof/doc_commit/temp_sweep_never_held.bend as PTempSweepNeverHeld
import ./proof/doc_commit/temp_sweep_only_own.bend as PTempSweepOnlyOwn
import ./proof/doc_commit/temp_sweep_removes_free.bend as PTempSweepRemovesFree
import ./proof/doc_commit/entry/list_met.bend as PDocCommitEntryListMet
import ./proof/doc_commit/entry/list_fate.bend as PDocCommitEntryListFate
import ./proof/doc_commit/entry/list_ents.bend as PDocCommitEntryListEnts
import ./proof/doc_commit/entry/fields.bend as PDocCommitEntryFields
import ./proof/doc_commit/commit_check_spec.bend as PCommitCheckSpec
import ./proof/doc_commit/commit_check_is_conflict.bend as PCommitCheckIsConflict
import ./proof/doc_commit/commit_outcome_spec.bend as PCommitOutcomeSpec
import ./proof/doc_commit/commit_outcome_is_publish.bend as PCommitOutcomeIsPublish
import ./proof/doc_commit/commit_answer_spec.bend as PCommitAnswerSpec
import ./proof/doc_commit/commit_answer_is_reply.bend as PCommitAnswerIsReply
import ./proof/doc_commit/commit_gate_spec.bend as PCommitGateSpec
import ./proof/doc_commit/commit_seen_spec.bend as PCommitSeenSpec
import ./proof/doc_commit/commit_prefix_spec.bend as PCommitPrefixSpec
import ./proof/doc_commit/commit_sweep_spec.bend as PCommitSweepSpec
import ./proof/doc_commit/commit_sweep_is_model.bend as PCommitSweepIsModel
import ./proof/doc_commit/commit_choices_example.bend as PCommitChoicesExample
import ./proof/doc_commit/commit_entry_reads.bend as PCommitEntryReads
import ./proof/doc_commit/commit_entry_answers.bend as PCommitEntryAnswers
import ./proof/doc_commit/commit_entry_exact.bend as PCommitEntryExact
import ./proof/doc_commit/commit_entry_refuses.bend as PCommitEntryRefuses
import ./proof/doc_commit/commit_entry_example.bend as PCommitEntryExample
import ./proof/doc_commit/write_unseen_spec.bend as PWriteUnseenSpec
import ./proof/doc_commit/write_saw_spec.bend as PWriteSawSpec
import ./proof/doc_lines/base.bend as LADocLines
import ./proof/doc_lines/load_persist_roundtrip.bend as PLoadPersistRoundtrip
import ./proof/doc_lines/edit_keeps_untouched_bytes.bend as PEditKeepsUntouchedBytes
import ./proof/doc_lines/edit_cut_points_exact.bend as PEditCutPointsExact
import ./proof/doc_lines/lines_carry_is_first_end.bend as PLinesCarryIsFirstEnd
import ./proof/doc_lines/edit_writes_new_lines.bend as PEditWritesNewLines
import ./proof/doc_lines/grep_line_is_read_line.bend as PGrepLineIsReadLine
import ./proof/doc_lines/persist_weaves_carry.bend as PPersistWeavesCarry
import ./proof/doc_lines/persist_writes_with_carry.bend as PPersistWritesWithCarry
import ./proof/doc_lines/edit_exact.bend as PEditExact
import ./proof/doc_lines/load_holds_first_end.bend as PLoadHoldsFirstEnd
import ./proof/doc_lines/persist_plan_refines.bend as PPersistPlanRefines
import ./proof/doc_lines/persist_plan_example.bend as PPersistPlanExample
import ./proof/doc_lines/lines_entry_refines.bend as PLinesEntryRefines
import ./proof/doc_lines/lines_entry_rejects_example.bend as PLinesEntryRejectsExample
import ./proof/doc_lines/lines_wire_fits_example.bend as PLinesWireFitsExample
import ./proof/doc_lines/lines_carry_is_first.bend as PLinesCarryIsFirst
import ./proof/doc_lines/lines_write_keeps.bend as PLinesWriteKeeps
import ./proof/doc_lines/lines_entry_answers.bend as PLinesEntryAnswers
import ./proof/doc_lines/lines_entry_exact.bend as PLinesEntryExact
import ./proof/doc_lines/lines_entry_example.bend as PLinesEntryExample
import ./proof/doc_lines/lines_req_fits_example.bend as PLinesReqFitsExample
import ./proof/doc_rows/base.bend as LADocRows
import ./proof/doc_rows/rows_lines_are_read_rows.bend as PRowsLinesAreReadRows
import ./proof/doc_rows/rows_raw_lines_are_pieces.bend as PRowsRawLinesArePieces
import ./proof/doc_rows/rows_gate_refuses.bend as PRowsGateRefuses
import ./proof/doc_rows/rows_view_shows.bend as PRowsViewShows
import ./proof/doc_rows/rows_view_example.bend as PRowsViewExample
import ./proof/doc_rows/rows_gap_marks_every_jump.bend as PRowsGapMarksEveryJump
import ./proof/doc_rows/rows_gap_example.bend as PRowsGapExample
import ./proof/doc_rows/rows_entry_answers.bend as PRowsEntryAnswers
import ./proof/doc_rows/rows_entry_exact.bend as PRowsEntryExact
import ./proof/doc_rows/rows_entry_example.bend as PRowsEntryExample
import ./proof/doc_rows/rows_req_fits_example.bend as PRowsReqFitsExample
import ./proof/doc_tags/tag_names_shown_text.bend as PTagNamesShownText
import ./proof/doc_tags/base.bend as LADocTags
import ./proof/doc_tags/grep_tag_fates_spec.bend as PGrepTagFatesSpec
import ./proof/doc_tags/tags_entry_answers.bend as PTagsEntryAnswers
import ./proof/doc_tags/tags_entry_reads.bend as PTagsEntryReads
import ./proof/doc_tags/tags_entry_exact.bend as PTagsEntryExact
import ./proof/doc_tags/tags_entry_refuses.bend as PTagsEntryRefuses
import ./proof/doc_tags/tags_entry_example.bend as PTagsEntryExample
import ./proof/doc_seen/base.bend as LADocSeen
import ./proof/doc_seen/edit_only_seen_lines.bend as PEditOnlySeenLines
import ./proof/doc_seen/edit_seen_applies.bend as PEditSeenApplies
import ./proof/doc_seen/reveal_then_retry.bend as PRevealThenRetry
import ./proof/doc_seen/edit_marks_whole_reveal.bend as PEditMarksWholeReveal
import ./proof/doc_seen/reject_names_unseen.bend as PRejectNamesUnseen
import ./proof/doc_seen/reject_shows_lines.bend as PRejectShowsLines
import ./proof/doc_seen/reject_whole_exact.bend as PRejectWholeExact
import ./proof/doc_seen/reveal_example.bend as PRevealExample
import ./proof/doc_seen/retry_few_witness.bend as PRetryFewWitness
import ./proof/doc_seen/retry_applies_example.bend as PRetryAppliesExample
import ./proof/doc_seen/retry_rejected_example.bend as PRetryRejectedExample
import ./proof/doc_seen/seen_runs_example.bend as PSeenRunsExample
import ./proof/doc_seen/reveal_bounds.bend as PRevealBounds
import ./proof/doc_seen/seen_entry_refines.bend as PSeenEntryRefines
import ./proof/doc_seen/seen_entry_rejects_example.bend as PSeenEntryRejectsExample
import ./proof/doc_seen/seen_wire_fits_example.bend as PSeenWireFitsExample
import ./proof/doc_search/base.bend as LADocSearch
import ./proof/doc_search/grep_accounts_every_file.bend as PGrepAccountsEveryFile
import ./proof/doc_search/grep_notes_every_gap.bend as PGrepNotesEveryGap
import ./proof/doc_search/grep_notes_every_cut.bend as PGrepNotesEveryCut
import ./proof/doc_search/continuation_progresses.bend as PContinuationProgresses
import ./proof/doc_search/continuation_contiguous.bend as PContinuationContiguous
import ./proof/doc_search/continuation_disjoint.bend as PContinuationDisjoint
import ./proof/doc_search/search_calls_example.bend as PSearchCallsExample
import ./proof/doc_search/search_walk_example.bend as PSearchWalkExample
import ./proof/doc_search/search_refuses_example.bend as PSearchRefusesExample
import ./proof/doc_search/page_is_window.bend as PPageIsWindow
import ./proof/doc_search/next_is_more.bend as PNextIsMore
import ./proof/doc_search/past_is_beyond.bend as PPastIsBeyond
import ./proof/doc_search/grep_scope_pages.bend as PGrepScopePages
import ./proof/doc_search/upto_counts.bend as PUptoCounts
import ./proof/doc_search/limit_cuts.bend as PLimitCuts
import ./proof/doc_search/fetch_reaches.bend as PFetchReaches
import ./proof/doc_search/grep_keeps_spec.bend as PGrepKeepsSpec
import ./proof/doc_search/grep_walk_spec.bend as PGrepWalkSpec
import ./proof/doc_search/limit_round_robin.bend as PLimitRoundRobin
import ./proof/doc_search/search_page_answers.bend as PSearchPageAnswers
import ./proof/doc_search/search_limit_answers.bend as PSearchLimitAnswers
import ./proof/doc_search/search_scope_answers.bend as PSearchScopeAnswers
import ./proof/doc_search/search_scope_rule.bend as PSearchScopeRule
import ./proof/doc_search/grep_account_exact.bend as PGrepAccountExact
import ./proof/doc_search/search_list_tests_exact.bend as PSearchListTestsExact
import ./proof/doc_search/search_note_count_exact.bend as PSearchNoteCountExact
import ./proof/doc_search/search_cuts_exact.bend as PSearchCutsExact
import ./proof/doc_search/search_open_answers.bend as PSearchOpenAnswers
import ./proof/doc_search/search_ask_stops.bend as PSearchAskStops
import ./proof/doc_search/search_ask_fetches.bend as PSearchAskFetches
import ./proof/doc_search/search_met_answers.bend as PSearchMetAnswers
import ./proof/doc_search/search_walk_runs.bend as PSearchWalkRuns
import ./proof/doc_search/search_shut_refuses.bend as PSearchShutRefuses
import ./proof/doc_search/search_step_refuses.bend as PSearchStepRefuses
import ./proof/doc_search/search_open_refuses.bend as PSearchOpenRefuses
import ./proof/doc_search/search_ffi_refuses.bend as PSearchFfiRefuses
import ./proof/doc_glob/base/rank.bend as LADocGlobRank
import ./proof/doc_glob/base/keep.bend as LADocGlobKeep
import ./proof/doc_glob/base/state.bend as LADocGlobState
import ./proof/doc_glob/base/steps.bend as LADocGlobSteps
import ./proof/doc_glob/glob_walk_runs.bend as PGlobWalkRuns
import ./proof/doc_glob/glob_events_answer.bend as PGlobEventsAnswer
import ./proof/doc_glob/glob_open_refuses.bend as PGlobOpenRefuses
import ./proof/doc_glob/glob_shut_refuses.bend as PGlobShutRefuses
import ./proof/doc_glob/glob_step_refuses.bend as PGlobStepRefuses
import ./proof/doc_glob/glob_walk_example.bend as PGlobWalkExample
import ./proof/doc_glob/glob_refuses_example.bend as PGlobRefusesExample
import ./proof/doc_glob/glob_fits_example.bend as PGlobFitsExample
import ./proof/config/base.bend as LAConfig
import ./proof/config/rmw_refuses_broken.bend as PRmwRefusesBroken
import ./proof/config/rmw_keeps_others.bend as PRmwKeepsOthers
import ./proof/config/rmw_applies_change.bend as PRmwAppliesChange
import ./proof/config/settings_save_preserves.bend as PSettingsSavePreserves
import ./proof/config/leaf_applied_or_reported.bend as PLeafAppliedOrReported
import ./proof/config/leaf_not_both.bend as PLeafNotBoth
import ./proof/config/limit_malformed_fails_closed.bend as PLimitMalformedFailsClosed
import ./proof/config/limit_number_applies.bend as PLimitNumberApplies
import ./proof/config/untrusted_changes_nothing_guarded.bend as PUntrustedChangesNothingGuarded
import ./proof/config/trusted_project_applies.bend as PTrustedProjectApplies
import ./proof/config/project_entry_never_merges.bend as PProjectEntryNeverMerges
import ./proof/config/global_entry_kept.bend as PGlobalEntryKept
import ./proof/default_model/base.bend as LADefaultModel
import ./proof/default_model/default_honoured_or_reported.bend as PDefaultHonouredOrReported
import ./proof/default_model/default_quiet_when_honoured.bend as PDefaultQuietWhenHonoured
import ./proof/default_model/default_quiet_when_unset.bend as PDefaultQuietWhenUnset
import ./proof/default_model/default_unkeyed_never_moves.bend as PDefaultUnkeyedNeverMoves
import ./proof/default_model/default_unset_runs_pick.bend as PDefaultUnsetRunsPick
import ./proof/default_model/default_unset_without_pick.bend as PDefaultUnsetWithoutPick
import ./proof/default_model/default_usable_runs.bend as PDefaultUsableRuns
import ./proof/default_model/default_uncatalogued_swaps.bend as PDefaultUncataloguedSwaps
import ./proof/default_model/default_uncatalogued_refused.bend as PDefaultUncataloguedRefused
import ./proof/default_model/default_unkeyed_refused.bend as PDefaultUnkeyedRefused
import ./proof/default_model/default_unscoped_swaps.bend as PDefaultUnscopedSwaps
import ./proof/default_model/default_unscoped_refused.bend as PDefaultUnscopedRefused
import ./proof/default_model/dmw_reason_round_trip.bend as PDmwReasonRoundTrip
import ./proof/default_model/dmw_pick_round_trip.bend as PDmwPickRoundTrip
import ./proof/default_model/dmw_sub_round_trip.bend as PDmwSubRoundTrip
import ./proof/default_model/dmw_res_round_trip.bend as PDmwResRoundTrip
import ./proof/default_model/dmw_answers.bend as PDmwAnswers
import ./proof/default_model/dmw_malformed.bend as PDmwMalformed
import ./proof/default_model/dmw_left_over.bend as PDmwLeftOver
import ./proof/default_model/dmw_reason_example.bend as PDmwReasonExample
import ./proof/default_model/dmw_saved_example.bend as PDmwSavedExample
import ./proof/default_model/dmw_next_example.bend as PDmwNextExample
import ./proof/default_model/dmw_in_example.bend as PDmwInExample
import ./proof/default_model/dmw_key_example.bend as PDmwKeyExample
import ./proof/default_model/dmw_pick_example.bend as PDmwPickExample
import ./proof/default_model/dmw_sub_example.bend as PDmwSubExample
import ./proof/default_model/dmw_res_example.bend as PDmwResExample
import ./proof/default_model/dmw_ffi_example.bend as PDmwFfiExample
import ./proof/default_model/dmw_malformed_example.bend as PDmwMalformedExample
import ./proof/workflow/base.bend as LAWorkflow
import ./proof/workflow/wf_running_within_concurrency.bend as PWfRunningWithinConcurrency
import ./proof/workflow/wf_spawned_within_budget.bend as PWfSpawnedWithinBudget
import ./proof/workflow/wf_cached_key_spawns_nothing.bend as PWfCachedKeySpawnsNothing
import ./proof/workflow/wf_empty_cache_spawns_all.bend as PWfEmptyCacheSpawnsAll
import ./proof/workflow/wf_failure_spares_siblings.bend as PWfFailureSparesSiblings
import ./proof/workflow/wf_admitted_never_respawns.bend as PWfAdmittedNeverRespawns
import ./proof/workflow/wf_reuses_first_answer.bend as PWfReusesFirstAnswer
import ./proof/workflow/wf_spawns_within_budget.bend as PWfSpawnsWithinBudget
import ./proof/workflow/wf_refused_when_spent.bend as PWfRefusedWhenSpent
import ./proof/workflow/wf_first_example.bend as PWfFirstExample
import ./proof/workflow/wf_limits_uncapped.bend as PWfLimitsUncapped
import ./proof/workflow/wf_limits_capped.bend as PWfLimitsCapped
import ./proof/workflow/wfw_sts_round_trip.bend as PWfwStsRoundTrip
import ./proof/workflow/wfw_admit_round_trip.bend as PWfwAdmitRoundTrip
import ./proof/workflow/wfw_decision_round_trip.bend as PWfwDecisionRoundTrip
import ./proof/workflow/wfw_limits_round_trip.bend as PWfwLimitsRoundTrip
import ./proof/workflow/wfw_answers_admit.bend as PWfwAnswersAdmit
import ./proof/workflow/wfw_answers_limits.bend as PWfwAnswersLimits
import ./proof/workflow/wfw_malformed.bend as PWfwMalformed
import ./proof/workflow/wfw_left_over.bend as PWfwLeftOver
import ./proof/workflow/wfw_tags_example.bend as PWfwTagsExample
import ./proof/workflow/wfw_prior_example.bend as PWfwPriorExample
import ./proof/workflow/wfw_row_example.bend as PWfwRowExample
import ./proof/workflow/wfw_rows_example.bend as PWfwRowsExample
import ./proof/workflow/wfw_pool_example.bend as PWfwPoolExample
import ./proof/workflow/wfw_admit_req_example.bend as PWfwAdmitReqExample
import ./proof/workflow/wfw_limits_req_example.bend as PWfwLimitsReqExample
import ./proof/workflow/wfw_admit_example.bend as PWfwAdmitExample
import ./proof/workflow/wfw_decision_example.bend as PWfwDecisionExample
import ./proof/workflow/wfw_limits_example.bend as PWfwLimitsExample
import ./proof/workflow/wfw_ffi_example.bend as PWfwFfiExample
import ./proof/workflow/wfw_malformed_example.bend as PWfwMalformedExample
import ./proof/command/base.bend as LACommand
import ./proof/command/command_path_runs_itself.bend as PCommandPathRunsItself
import ./proof/command/command_unknown_runs_nothing.bend as PCommandUnknownRunsNothing
import ./proof/command/command_free_takes_rest.bend as PCommandFreeTakesRest
import ./proof/command/command_stray_is_not_a_command.bend as PCommandStrayIsNotACommand
import ./proof/command/command_memory_model_example.bend as PCommandMemoryModelExample
import ./proof/command/command_memory_model_keys_example.bend as PCommandMemoryModelKeysExample
import ./proof/command/command_menu_lists_children.bend as PCommandMenuListsChildren
import ./proof/command/command_menu_names_first_word.bend as PCommandMenuNamesFirstWord
import ./proof/command/command_menu_shut_off_path.bend as PCommandMenuShutOffPath
import ./proof/command/command_tab_completes_row.bend as PCommandTabCompletesRow
import ./proof/command/command_enter_on_row.bend as PCommandEnterOnRow
import ./proof/command/command_enter_without_row.bend as PCommandEnterWithoutRow
import ./proof/command/command_tab_without_row.bend as PCommandTabWithoutRow
import ./proof/command/command_stale_row_ignored.bend as PCommandStaleRowIgnored
import ./proof/command/command_ffi_round_trip.bend as PCommandFfiRoundTrip
import ./proof/command/command_ffi_answers.bend as PCommandFfiAnswers
import ./proof/command/command_ffi_left_over.bend as PCommandFfiLeftOver
import ./proof/command/command_ffi_malformed.bend as PCommandFfiMalformed
import ./proof/command/command_ffi_res_round_trip.bend as PCommandFfiResRoundTrip
import ./proof/command/command_ffi_menu_round_trip.bend as PCommandFfiMenuRoundTrip
import ./proof/command/command_ffi_out_round_trip.bend as PCommandFfiOutRoundTrip
import ./proof/command/command_ffi_witness.bend as PCommandFfiWitness
import ./proof/shell/base.bend as LAShell
import ./proof/shell/shell_ffi_exact.bend as PShellFfiExact
import ./proof/shell/shell_ffi_answers.bend as PShellFfiAnswers
import ./proof/shell/shell_ffi_left_over.bend as PShellFfiLeftOver
import ./proof/shell/shell_ffi_example.bend as PShellFfiExample
import ./proof/runners/base/entry.bend as LARunnersEntry
import ./proof/runners/runners_ffi_exact.bend as PRunnersFfiExact
import ./proof/runners/runners_ffi_answers.bend as PRunnersFfiAnswers
import ./proof/runners/runners_ffi_left_over.bend as PRunnersFfiLeftOver
import ./proof/runners/runners_ffi_example.bend as PRunnersFfiExample
import ./proof/approvals/base/entry.bend as LAApprovalsEntry
import ./proof/approvals/approvals_ffi_exact.bend as PApprovalsFfiExact
import ./proof/approvals/approvals_ffi_answers.bend as PApprovalsFfiAnswers
import ./proof/approvals/approvals_ffi_left_over.bend as PApprovalsFfiLeftOver
import ./proof/approvals/approvals_ffi_example.bend as PApprovalsFfiExample
import ./proof/sandbox/base/frames.bend as LASandboxFrames
import ./proof/sandbox/frames_admit_seen.bend as PFramesAdmitSeen
import ./proof/sandbox/frames_admit_oversize.bend as PFramesAdmitOversize
import ./proof/sandbox/frames_admit_within.bend as PFramesAdmitWithin
import ./proof/sandbox/frames_admit_serves_accepted.bend as PFramesAdmitServesAccepted
import ./proof/sandbox/frames_ffi_exact.bend as PFramesFfiExact
import ./proof/sandbox/frames_ffi_answers.bend as PFramesFfiAnswers
import ./proof/sandbox/frames_ffi_left_over.bend as PFramesFfiLeftOver
import ./proof/sandbox/frames_ffi_example.bend as PFramesFfiExample
import ./proof/tool_surface/base.bend as LAToolSurface
import ./proof/tool_surface/tool_surface_ffi_exact.bend as PToolSurfaceFfiExact
import ./proof/tool_surface/tool_surface_ffi_answers.bend as PToolSurfaceFfiAnswers
import ./proof/tool_surface/tool_surface_ffi_left_over.bend as PToolSurfaceFfiLeftOver
import ./proof/tool_surface/tool_surface_ffi_example.bend as PToolSurfaceFfiExample
import ./proof/sandbox/frames_verdict_serve_exact.bend as PFramesVerdictServeExact
import ./proof/infer_force/infer_force_flag_exact.bend as PInferForceFlagExact
import ./proof/infer_force/infer_force_after_exact.bend as PInferForceAfterExact
import ./proof/infer_force/infer_force_steps.bend as PInferForceSteps
import ./proof/infer_force/infer_force_ffi_flag.bend as PInferForceFfiFlag
import ./proof/infer_force/infer_force_ffi_after.bend as PInferForceFfiAfter
import ./proof/infer_force/infer_force_ffi_malformed_exact.bend as PInferForceFfiMalformedExact
import ./proof/infer_force/infer_force_ffi_example.bend as PInferForceFfiExample
import ./proof/infer_guard/base.bend as LAInferGuard
import ./proof/infer_guard/infer_guard_start_exact.bend as PInferGuardStartExact
import ./proof/infer_guard/infer_guard_feed_exact.bend as PInferGuardFeedExact
import ./proof/infer_guard/infer_guard_steps.bend as PInferGuardSteps
import ./proof/infer_guard/infer_guard_ffi_open.bend as PInferGuardFfiOpen
import ./proof/infer_guard/infer_guard_ffi_open_malformed_exact.bend as PInferGuardFfiOpenMalformedExact
import ./proof/infer_guard/infer_guard_ffi_step.bend as PInferGuardFfiStep
import ./proof/infer_guard/infer_guard_ffi_step_malformed_exact.bend as PInferGuardFfiStepMalformedExact
import ./proof/infer_guard/infer_guard_ffi_ended.bend as PInferGuardFfiEnded
import ./proof/infer_guard/infer_guard_ffi_shut.bend as PInferGuardFfiShut
import ./proof/infer_guard/infer_guard_ffi_example.bend as PInferGuardFfiExample
import ./proof/infer_threshold/base.bend as LAInferThreshold
import ./proof/infer_threshold/infer_threshold_over_exact.bend as PInferThresholdOverExact
import ./proof/infer_threshold/infer_threshold_blocks_steps.bend as PInferThresholdBlocksSteps
import ./proof/infer_threshold/infer_threshold_early_steps.bend as PInferThresholdEarlySteps
import ./proof/infer_threshold/infer_threshold_ffi_answers.bend as PInferThresholdFfiAnswers
import ./proof/infer_threshold/infer_threshold_ffi_malformed_exact.bend as PInferThresholdFfiMalformedExact
import ./proof/infer_threshold/infer_threshold_ffi_example.bend as PInferThresholdFfiExample
import ./proof/bound/base.bend as LABound
import ./proof/bound/bound_entry_example.bend as PBoundEntryExample
import ./proof/bound/bound_ffi_malformed_exact.bend as PBoundFfiMalformedExact
import ./proof/bound/bound_ffi_notice.bend as PBoundFfiNotice
import ./proof/bound/bound_ffi_slice.bend as PBoundFfiSlice
import ./proof/bound/bound_head_full_keeps.bend as PBoundHeadFullKeeps
import ./proof/bound/bound_keep_exact.bend as PBoundKeepExact
import ./proof/bound/bound_look_exact.bend as PBoundLookExact
import ./proof/bound/bound_margin_exact.bend as PBoundMarginExact
import ./proof/bound/bound_notice_exact.bend as PBoundNoticeExact
import ./proof/bound/bound_open_answers.bend as PBoundOpenAnswers
import ./proof/bound/bound_open_refuses.bend as PBoundOpenRefuses
import ./proof/bound/bound_out_exact.bend as PBoundOutExact
import ./proof/bound/bound_shut_refuses.bend as PBoundShutRefuses
import ./proof/bound/bound_skip_exact.bend as PBoundSkipExact
import ./proof/bound/bound_slice_conserves.bend as PBoundSliceConserves
import ./proof/bound/bound_slice_exact.bend as PBoundSliceExact
import ./proof/bound/bound_step_look.bend as PBoundStepLook
import ./proof/bound/bound_step_out.bend as PBoundStepOut
import ./proof/bound/bound_step_refuses.bend as PBoundStepRefuses
import ./proof/bound/bound_step_skip.bend as PBoundStepSkip
import ./proof/bound/bound_steps_whole.bend as PBoundStepsWhole
import ./proof/bound/bound_window_exact.bend as PBoundWindowExact
import ./proof/bound/bound_window_keeps_what_fits.bend as PBoundWindowKeepsWhatFits
import ./proof/bound/bound_window_within.bend as PBoundWindowWithin
import ./proof/selection/base.bend as LASelection
import ./proof/selection/sel_release_copies/row.bend as LASelectionRow
import ./proof/selection/sel_release_copies.bend as PSelReleaseCopies
import ./proof/selection/sel_copy_anchor_to_head.bend as PSelCopyAnchorToHead
import ./proof/selection/sel_wrap_joins.bend as PSelWrapJoins
import ./proof/selection/sel_wrap_trailing_blanks_example.bend as PSelWrapTrailingBlanksExample
import ./proof/selection/sel_release_copies_once.bend as PSelReleaseCopiesOnce
import ./proof/selection/sel_click_copies_nothing.bend as PSelClickCopiesNothing
import ./proof/selection/sel_single_press.bend as PSelSinglePress
import ./proof/selection/sel_word_bounds.bend as PSelWordBounds
import ./proof/selection/sel_line_bounds.bend as PSelLineBounds
import ./proof/selection/sel_drag_moves_head.bend as PSelDragMovesHead
import ./proof/selection/sel_scroll_past_edge.bend as PSelScrollPastEdge
import ./proof/selection/sel_key_clears.bend as PSelKeyClears
import ./proof/selection/sel_esc_clears.bend as PSelEscClears
import ./proof/selection/selection_ffi_decides.bend as PSelectionFfiDecides
import ./proof/selection/selection_ffi_open.bend as PSelectionFfiOpen
import ./proof/selection/selection_ffi_example.bend as PSelectionFfiExample
import ./proof/selection/selection_ffi_left_over.bend as PSelectionFfiLeftOver
import ./proof/selection/selection_ffi_error_keeps_the_state.bend as PSelectionFfiErrorKeepsTheState
import ./proof/selection/selection_ffi_reads_only_events.bend as PSelectionFfiReadsOnlyEvents
import ./proof/selection/selection_ffi_unknown_event.bend as PSelectionFfiUnknownEvent
import ./proof/selection/selection_ffi_unknown_wrap.bend as PSelectionFfiUnknownWrap
import ./proof/codemode_id/base.bend as LACodemodeId
import ./proof/codemode_id/codemode_id_exact.bend as PCodemodeIdExact
import ./proof/codemode_id/codemode_id_is_identifier.bend as PCodemodeIdIsIdentifier
import ./proof/codemode_id/codemode_id_keeps_identifiers.bend as PCodemodeIdKeepsIdentifiers
import ./proof/codemode_id/codemode_id_example.bend as PCodemodeIdExample
import ./proof/codemode_id/codemode_id_is_exact.bend as PCodemodeIdIsExact
import ./proof/codemode_id/codemode_id_is_example.bend as PCodemodeIdIsExample
import ./proof/codemode_id/codemode_id_ffi_answers.bend as PCodemodeIdFfiAnswers
import ./proof/codemode_id/codemode_id_ffi_is.bend as PCodemodeIdFfiIs
import ./proof/codemode_id/codemode_id_ffi_exact.bend as PCodemodeIdFfiExact
import ./proof/codemode_id/codemode_id_ffi_malformed.bend as PCodemodeIdFfiMalformed
import ./proof/codemode_id/codemode_id_ffi_left_over.bend as PCodemodeIdFfiLeftOver
import ./proof/codemode_id/codemode_id_ffi_example.bend as PCodemodeIdFfiExample
import ./proof/submission/base.bend as LASubmission
import ./proof/submission/submission_step_exact.bend as PSubmissionStepExact
import ./proof/submission/submission_settled_stays.bend as PSubmissionSettledStays
import ./proof/submission/submission_moves_forward.bend as PSubmissionMovesForward
import ./proof/submission/submission_example.bend as PSubmissionExample
import ./proof/submission/submission_ffi_example.bend as PSubmissionFfiExample
import ./proof/submission/submission_ffi_answers.bend as PSubmissionFfiAnswers
import ./proof/submission/submission_ffi_left_over.bend as PSubmissionFfiLeftOver
import ./proof/submission/submission_ffi_exact.bend as PSubmissionFfiExact
import ./proof/scan/base.bend as LAScan
import ./proof/scan/scan_start_exact.bend as PScanStartExact
import ./proof/scan/scan_cursor_keeps_its_order.bend as PScanCursorKeepsItsOrder
import ./proof/scan/scan_id_exact.bend as PScanIdExact
import ./proof/scan/scan_start_example.bend as PScanStartExample
import ./proof/scan/scan_ffi_example.bend as PScanFfiExample
import ./proof/scan/scan_ffi_answers.bend as PScanFfiAnswers
import ./proof/scan/scan_ffi_left_over.bend as PScanFfiLeftOver
import ./proof/scan/scan_ffi_exact.bend as PScanFfiExact
import ./proof/scan/scan_ffi_malformed_exact.bend as PScanFfiMalformedExact
import ./proof/scan/scan_ffi_read_example.bend as PScanFfiReadExample
import ./proof/submission/submission_ffi_malformed_exact.bend as PSubmissionFfiMalformedExact
import ./proof/submission/submission_ffi_read_example.bend as PSubmissionFfiReadExample
import ./proof/wire/wire_nat_decimal.bend as PWireNatDecimal
import ./proof/wire/wire_strs_example.bend as PWireStrsExample
import ./proof/wire/base/spell.bend as LAWireSpell
import ./proof/wire/wire_strs_spells.bend as PWireStrsSpells
import ./proof/wire/wire_nats_spells.bend as PWireNatsSpells
import ./proof/wire/wire_strs_round_trip.bend as PWireStrsRoundTrip
import ./proof/wire/wire_strs_exact.bend as PWireStrsExact
import ./proof/wire/wire_str_decoded_fits.bend as PWireStrDecodedFits
import ./proof/wire/wire_strs_decoded_fit.bend as PWireStrsDecodedFit
import ./proof/command/command_ffi_example.bend as PCommandFfiExample
import ./proof/command/command_spacing_example.bend as PCommandSpacingExample
import ./proof/command/base/entry.bend as LACommandEntry
import ./proof/command/command_ffi_decides.bend as PCommandFfiDecides
import ./proof/command/command_ffi_spelled_left_over.bend as PCommandFfiSpelledLeftOver
import ./proof/command/command_ffi_unknown_query.bend as PCommandFfiUnknownQuery
import ./proof/command/command_ffi_unknown_row.bend as PCommandFfiUnknownRow
import ./proof/command/command_ffi_unknown_press.bend as PCommandFfiUnknownPress
import ./proof/command/command_ffi_unknown_res.bend as PCommandFfiUnknownRes
import ./proof/command/command_ffi_unknown_menu.bend as PCommandFfiUnknownMenu
import ./proof/command/command_ffi_res_reads_spelled.bend as PCommandFfiResReadsSpelled
import ./proof/command/command_ffi_menu_reads_spelled.bend as PCommandFfiMenuReadsSpelled
import ./proof/command/command_ffi_out_reads_spelled.bend as PCommandFfiOutReadsSpelled
import ./proof/command/command_ffi_reads_only_requests.bend as PCommandFfiReadsOnlyRequests
import ./proof/command/command_ffi_malformed_unless_request.bend as PCommandFfiMalformedUnlessRequest
import ./proof/command/base/space.bend as LACommandSpace
import ./proof/command/base/named.bend as LACommandNamed
import ./proof/command/command_named_example.bend as PCommandNamedExample
import ./proof/command/command_named_dup_example.bend as PCommandNamedDupExample
import ./proof/command/command_named_premises_witness.bend as PCommandNamedPremisesWitness
import ./proof/command/command_named_word_resolves.bend as PCommandNamedWordResolves
import ./proof/command/command_named_word_menu.bend as PCommandNamedWordMenu
import ./proof/command/command_named_word_ends.bend as PCommandNamedWordEnds
import ./proof/command/command_named_word_menu_any.bend as PCommandNamedWordMenuAny
import ./proof/command/command_named_word_resolves_alike.bend as PCommandNamedWordResolvesAlike
import ./proof/command/command_named_word_then_blank.bend as PCommandNamedWordThenBlank
import ./proof/command/command_named_word_then_child.bend as PCommandNamedWordThenChild
import ./proof/command/command_named_word_then_other.bend as PCommandNamedWordThenOther
import ./proof/command/command_key_follows_menu.bend as PCommandKeyFollowsMenu
import ./proof/command/command_row_ignored_shut_menu.bend as PCommandRowIgnoredShutMenu
import ./proof/command/command_blank_runs_nothing.bend as PCommandBlankRunsNothing
import ./proof/command/command_space_lead.bend as PCommandSpaceLead
import ./proof/command/command_tab_row_any_spacing.bend as PCommandTabRowAnySpacing
import ./proof/command/command_enter_row_any_spacing.bend as PCommandEnterRowAnySpacing
import ./proof/command/command_stale_row_any_spacing.bend as PCommandStaleRowAnySpacing
import ./proof/command/command_space_trailing.bend as PCommandSpaceTrailing
import ./proof/command/command_space_gap.bend as PCommandSpaceGap
import ./proof/command/command_menu_space_gap.bend as PCommandMenuSpaceGap
import ./proof/command/command_menu_space_lead.bend as PCommandMenuSpaceLead
import ./proof/command/command_menu_space_lead_word.bend as PCommandMenuSpaceLeadWord
import ./proof/command/command_row_ignored_off_path.bend as PCommandRowIgnoredOffPath
import ./proof/command/command_premises_witness.bend as PCommandPremisesWitness
import ./proof/command/command_ffi_premises_witness.bend as PCommandFfiPremisesWitness
import ./proof/retry_note/base.bend as LARetryNote
import ./proof/retry_note/retry_note_exact.bend as PRetryNoteExact
import ./proof/retry_note/retry_note_example.bend as PRetryNoteExample
import ./proof/retry_note/retry_note_limit_example.bend as PRetryNoteLimitExample
import ./proof/retry_note/retry_note_ffi_answers.bend as PRetryNoteFfiAnswers
import ./proof/retry_note/retry_note_ffi_left_over.bend as PRetryNoteFfiLeftOver
import ./proof/retry_note/retry_note_ffi_exact.bend as PRetryNoteFfiExact
import ./proof/retry_note/retry_note_ffi_left_over_exact.bend as PRetryNoteFfiLeftOverExact
import ./proof/retry_note/retry_note_ffi_errors.bend as PRetryNoteFfiErrors
import ./proof/retry_note/retry_note_ffi_example.bend as PRetryNoteFfiExample
import ./proof/doc_plan/base.bend as LADocPlan
import ./proof/doc_plan/doc_plan_content_exact.bend as PDocPlanContentExact
import ./proof/doc_plan/doc_plan_publishes_exact.bend as PDocPlanPublishesExact
import ./proof/doc_plan/doc_plan_example.bend as PDocPlanExample
import ./proof/doc_plan/doc_plan_ffi_answers.bend as PDocPlanFfiAnswers
import ./proof/doc_plan/doc_plan_ffi_left_over.bend as PDocPlanFfiLeftOver
import ./proof/doc_plan/doc_plan_ffi_exact.bend as PDocPlanFfiExact
import ./proof/doc_plan/doc_plan_ffi_left_over_exact.bend as PDocPlanFfiLeftOverExact
import ./proof/doc_plan/doc_plan_ffi_errors.bend as PDocPlanFfiErrors
import ./proof/doc_plan/doc_plan_ffi_example.bend as PDocPlanFfiExample