From 06abaeff793ac8cd3452a8906214bbbf5254d31f Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 30 Jul 2026 12:30:30 +0200 Subject: [PATCH] verification: close the two-button seam and level up the scalar button (P0-b) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit THE SEAM. This repository is checked by two scripts, and until now neither asserted anything about the other's scope. check.sh's dead-file gate simply SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by nothing at all: absent from one manifest by exemption, from the other by omission, compiled by neither, inventoried by neither. Each button now reads the other's manifest and requires every shipped proof source to belong to EXACTLY ONE of them — neither orphaned nor double-claimed, both directions, plus a phantom check on entries naming files that do not exist. Negative-tested four ways, including the exact hole this item names. THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link, having been left behind by every hardening round while the main button gained five phases. 45 lines to 227: - source-integrity check over its sources; - harness-pin verification, so running THIS button alone is protected and not only running it after check.sh; - a kernel-side axiom-declaration gate over the compiled artifacts, replacing a source-text grep that is evadable four ways on v4.30.0-rc2; - a declaration inventory of ~1880 constants against its own allowlist, diffed both directions with a count trailer. These 13 modules were the only part of the proof corpus with no inventory: check.sh Phase 2c named them as uncovered on every run, and now names the button that covers them instead; - per-certificate exact-cone assertions replacing `-eq 13` over matching output lines. A count cannot say WHICH certificate is clean and passes just as happily if one cone is reported twice. Every fork-specific fact was read from the existing script rather than assumed: risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit cond_add_l_one_spec, untouched. THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer and owned by the main button. - the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be scalar-owned. REMOVED rather than special-cased: the seam check tests membership in exactly one manifest, which is strictly stronger than any prefix; - the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a 13-module manifest. On a tree where check.sh had not run that artifact is absent and the button would have failed for a false reason. It now scans the manifest by membership and fails closed on a missing artifact; - Phase 2c's driver discovery globbed Inventory*.lean and claimed the other button's driver, then correctly complained its own manifest lacked those modules. This is the family the campaign began with: a source-text axiom grep reasoning about spelling. Recorded in TRUSTED-BASE.md because it generalises. Also fixed: the first negative test of the scalar gate's absence check passed for the wrong reason — the button recompiles before the gate runs, so removing an artifact merely caused it to be rebuilt. Retested against the lifted phase, where absence is a persistent condition. Verified green: 24 runs across the four repositories — four main buttons, four scalar buttons, and sixteen self-tests — zero red. Co-Authored-By: Claude Opus 4.8 --- TRUSTED-BASE.md | 31 + verification/HARNESS.sha256 | 6 +- verification/Proofs/InventoryScalar.lean | 30 + verification/check-scalar.sh | 229 ++- verification/check.sh | 56 +- verification/inventory-allowlist-scalar.txt | 1894 +++++++++++++++++++ 6 files changed, 2220 insertions(+), 26 deletions(-) create mode 100644 verification/Proofs/InventoryScalar.lean create mode 100644 verification/inventory-allowlist-scalar.txt diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 4a182a3..b650655 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -144,3 +144,34 @@ running Rust code. Everything else is machine-checked. is the two-button seam, still open. Phase 2c prints every uncovered module by name on every run, so the omission is visible rather than inferred. + +11. **Both buttons, and the seam between them.** This repository is checked by + two scripts: `check.sh` covers the field, curve and signature layers, + `check-scalar.sh` the scalar layer. Until 2026-07-30 neither asserted + anything about the other's scope and the main one simply SKIPPED anything + named `Scalar*`, so a new `Proofs/ScalarX.lean` was gated by nothing at all + — absent from one manifest by exemption, from the other by omission, + compiled by neither, inventoried by neither. Each button now reads the + other's manifest and requires every shipped proof source to belong to + EXACTLY ONE of them, both directions: neither orphaned nor double-claimed. + + The scalar button was also brought to the main one's standard, having been + left behind by every hardening round: it now checks source integrity, + verifies the harness pins (so running it alone is protected too), asks the + KERNEL about axiom declarations instead of grepping source text, inventories + its ~1,880 declarations against its own allowlist, and asserts each of its + 13 certificates by name rather than counting how many lines of output + matched. A count cannot say WHICH certificate is clean, and passes just as + happily if one cone is reported twice. + + **What this cost, recorded because the lesson generalises.** Three separate + gates in this work reasoned about how a thing is SPELLED rather than what it + BELONGS TO, and the corpus punished each one: `Proofs/ScalarPackSpec.lean` + is named like the scalar layer and owned by the main button. A dead-file + gate globbing `Scalar*` demanded it be scalar-owned; an axiom gate scanning + `Scalar*.olean` swept in an artifact this button does not compile, which on + a fresh tree is absent and would have failed the run for a false reason; and + the inventory driver discovery globbing `Inventory*.lean` claimed the other + button's driver. All three now test membership in a manifest. This is the + same family as the source-text axiom grep that began this campaign: + reasoning about names instead of about the thing itself. diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index f8edd2e..1ad24f6 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,14 +1,16 @@ 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt -b88f4bc16d3188f4830f8333201fc7826d46acf829c37f7da398d6ae9bfca15e check-scalar.sh -c0062555569ee4287770385ab5a1923d1028888e1bb62a32a52c33305c1a3222 check.sh +d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh +27b84e22853e381c31bb89ccf38ac333ec13ff1eadc5828eabf9c8f577e79a15 check.sh 7a55136cd15ab96b3ab77234ffb8a2fc7c9544cb8b36426d29e257ffb2d2ba6e extract.sh c9672a28825cd1d4055fb9efbb4a1d94c921c7b5c79e4cd5d0626ba061e554c1 GEN-MODEL.sha256 +e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05 inventory-allowlist-scalar.txt 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean 84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean 4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc Proofs/Inventory.lean +6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean 62da1de45d2e19abe588a75e32454548e8caa3067ff51a97d7ae155886dbe0c0 selftest-axgate.sh 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh diff --git a/verification/Proofs/InventoryScalar.lean b/verification/Proofs/InventoryScalar.lean new file mode 100644 index 0000000..61e4613 --- /dev/null +++ b/verification/Proofs/InventoryScalar.lean @@ -0,0 +1,30 @@ +/- ────────────────────────────────────────────────────────────────────────── + Proofs/InventoryScalar.lean — declaration inventory for the scalar layer. + + Audit INFRASTRUCTURE, not corpus. Compiled by check-scalar.sh Phase 2c, + which is where these modules' compiled artifacts exist: check.sh does not + compile the scalar layer, so its own inventory could not cover them and + named them as uncovered on every run instead. This closes that. +────────────────────────────────────────────────────────────────────────── -/ +import Proofs.InventoryCore +import Proofs.ScalarDenote +import Proofs.ScalarLoop +import Proofs.ScalarSubSpec +import Proofs.ScalarAddSpec +import Proofs.ScalarMulSpec +import Proofs.ScalarMontSpec +import Proofs.ScalarReduceSpec +import Proofs.ScalarFullMulSpec +import Proofs.ScalarMain +import Proofs.ScalarWideSpec +import Proofs.ScalarBytesSpec +import Proofs.ScalarUnpackSpec +import Proofs.ScalarFromBytesSpec +open Lean Ed25519Inventory + +/-- Exactly check-scalar.sh's PROOFS manifest; that script asserts the + correspondence in both directions. -/ +def corpus : Array Name := + #[`Proofs.ScalarDenote, `Proofs.ScalarLoop, `Proofs.ScalarSubSpec, `Proofs.ScalarAddSpec, `Proofs.ScalarMulSpec, `Proofs.ScalarMontSpec, `Proofs.ScalarReduceSpec, `Proofs.ScalarFullMulSpec, `Proofs.ScalarMain, `Proofs.ScalarWideSpec, `Proofs.ScalarBytesSpec, `Proofs.ScalarUnpackSpec, `Proofs.ScalarFromBytesSpec] + +#eval show MetaM Unit from emitInventory corpus diff --git a/verification/check-scalar.sh b/verification/check-scalar.sh index 2e3c1f1..00d972e 100755 --- a/verification/check-scalar.sh +++ b/verification/check-scalar.sh @@ -1,45 +1,232 @@ #!/usr/bin/env bash -# Scalar-layer check (Scalar52 arithmetic mod ℓ) — the layer is COMPLETE: -# add, sub, Montgomery mul, and the byte-parsing chain, all kernel-audited. +# ───────────────────────────────────────────────────────────────────────────── +# check-scalar.sh — THE SECOND BUTTON (Scalar52 arithmetic mod ℓ). +# # Runs against the merged gen/CurveField universe (the scalar module lives # there since the merge; see extract.sh). Guarded compiles throughout. +# +# Brought to the same standard as check.sh on 2026-07-30 (P0-b). Before that +# it was the weakest link in the estate, and increasingly so as the main button +# was hardened: no source-integrity check, no harness pin, no dead-file gate, +# no declaration inventory, an EVADABLE source-text grep for axioms where the +# main button asks the kernel, and a count of matching output lines where the +# main button asserts each certificate's cone individually. +# +# Phases: +# 0 source integrity + harness pin (so running this button alone is also +# protected, not only running it after check.sh) +# 1 the two-button seam: every shipped proof source belongs to exactly one +# of the two manifests, asserted against check.sh's, both directions +# 2 compile the scalar layer, with a dead-file gate over Scalar* +# 2b kernel-side axiom-declaration gate over the compiled artifacts +# 2c environment-derived declaration inventory, diffed both directions +# 3 per-certificate exact-cone audit +# ───────────────────────────────────────────────────────────────────────────── set -uo pipefail source ~/aeneas-toolchain/env.sh HERE="$(cd "$(dirname "$0")" && pwd)" AENEAS_LEAN="$AENEAS_HOME/backends/lean" -GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs) # MERGED GEN: scalar module now lives in CurveField +TIMEOUT="${LEAN_TIMEOUT:-300}" +CORES="${LEAN_MAX_CORES:-0-3}" +GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs) PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec) +# Fully-qualified scalar certificates. Each must report EXACTLY the standard +# three axioms — asserted per certificate, not by counting how many lines of +# output happened to match. A count cannot tell you WHICH certificate is clean. +CERTS=( + ScalarProofs.L_val + ScalarProofs.sub_loop_spec + ScalarProofs.sub_loop1_one_spec + ScalarProofs.sub_val_spec + ScalarProofs.add_val_spec + ScalarProofs.mul_internal_spec + ScalarProofs.part1_spec + ScalarProofs.montgomery_reduce_spec + ScalarProofs.mul_spec + ScalarProofs.scalarImplementation + ScalarProofs.montgomery_mul_spec + ScalarProofs.bytes_unpack_spec + ScalarProofs.from_bytes_wide_spec +) +EXPECTED="[propext, Classical.choice, Quot.sound]" -echo "=== stub/axiom audit ===" -grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; } -echo " clean" -echo "=== compile (guarded) ===" +# ── Phase 0: source integrity + harness pin ───────────────────────────────── +echo "=== Phase 0: source integrity + harness pin ===" +free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}' || exit 1 +for f in "$HERE"/Proofs/Scalar*.lean; do + [ -f "$f" ] || continue + if ! grep -qE '^(/-|import |namespace |theorem |def |open |set_option |--)' "$f"; then + echo "CORRUPTED: $f is not Lean source (olean clobber?). Restore: git checkout HEAD -- $f" + exit 1 + fi +done +# The pin file and its policy live with check.sh; this button verifies the same +# pins so that running it ALONE is protected too. If check.sh is absent the +# harness is not pinned and that is a hard stop, not a warning. +if [ ! -s "$HERE/HARNESS.sha256" ]; then + echo "FATAL: HARNESS.sha256 is missing or empty — the harness is unpinned."; exit 1 +fi +if ! ( cd "$HERE" && sha256sum -c --quiet HARNESS.sha256 ) ; then + echo "FATAL: a harness file does not match its pin. The button you are running" + echo "is not the button that was reviewed."; exit 1 +fi +echo " sources valid; $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins" + +# ── Phase 1: the two-button seam ──────────────────────────────────────────── +# The mirror of check.sh's Phase 1b. Each button reads the other's manifest, so +# a new Proofs/ScalarX.lean cannot be absent from one by exemption and from the +# other by omission — which is exactly what it was until today. +echo "=== Phase 1: two-button seam ===" +SEAMFAIL=0 +MAIN_SH="$HERE/check.sh" +if [ ! -f "$MAIN_SH" ]; then + echo " FATAL: check.sh is absent — most of the corpus would go unchecked."; exit 1 +fi +MAIN_MANIFEST=$(sed -n '/^PROOFS=(/,/^)/p' "$MAIN_SH" | grep -oE '^ [A-Za-z][A-Za-z0-9]*' | tr -d ' ' | sort -u) +if [ -z "$MAIN_MANIFEST" ]; then + echo " FATAL: could not read check.sh's manifest; refusing to guess its scope."; exit 1 +fi +SCALAR_MANIFEST=$(printf '%s\n' "${PROOFS[@]}" | sort -u) +for f in "$HERE"/Proofs/*.lean; do + b=$(basename "$f" .lean) + case "$b" in AxiomCheck|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac + inm=0; ins=0 + grep -qx "$b" <<<"$MAIN_MANIFEST" && inm=1 + grep -qx "$b" <<<"$SCALAR_MANIFEST" && ins=1 + if [ $((inm + ins)) -eq 0 ]; then + echo " ORPHAN: Proofs/$b.lean is in NEITHER manifest — compiled and audited by no button"; SEAMFAIL=1 + elif [ $((inm + ins)) -eq 2 ]; then + echo " DOUBLE-CLAIMED: Proofs/$b.lean is in BOTH manifests"; SEAMFAIL=1 + fi +done +[ "$SEAMFAIL" = 0 ] && echo " every proof source belongs to exactly one button" +[ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; } + +# ── Phase 2: compile ──────────────────────────────────────────────────────── +echo "=== Phase 2: compile (guarded) ===" cd "$AENEAS_LEAN" lake env bash -c " set -uo pipefail cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" - for m in ${GEN[*]}; do echo \" · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done + for m in ${GEN[*]}; do echo \" · gen \$m\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done cd '$HERE' - for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done + for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done + # NO NAME-PREFIX DEAD-FILE GATE HERE. A Scalar* NAME does not imply this + # button owns the file: Proofs/ScalarPackSpec.lean is in check.sh's manifest, + # and a prefix gate demanded it be in this one. Phase 1 above is the correct + # test and strictly stronger — it requires every proof source to be in + # EXACTLY ONE of the two manifests, by membership rather than by spelling. " || { echo FAIL; exit 1; } -echo "=== Phase 3: axiom audit (kernel-level) ===" + +# ── Phase 2b: kernel-side axiom-declaration gate ──────────────────────────── +# The source-text grep this button used until today is evadable four ways on +# Lean v4.30.0-rc2 (indented, @[simp], unsafe, and name-on-the-next-line — all +# compile, none match an anchored pattern). Ask the kernel instead, reading the +# compiled artifacts, exactly as check.sh Phase 2b does. +echo "=== Phase 2b: kernel-side axiom-declaration gate ===" +# The scanned set is this button's MANIFEST, not everything spelled Scalar*. +# Proofs/ScalarPackSpec.lean is compiled by check.sh, so a glob swept in an +# artifact this button does not own — and on a tree where check.sh had not run, +# that olean is absent and the coverage count would fail for a false reason. +SCALAR_OLEANS=$(printf '"%s.olean", ' "${PROOFS[@]}" | sed 's/, $//') +GATE=$(mktemp "$HERE/.axgate-scalar-XXXX.lean") +{ + echo "import Lean" + echo "open Lean" + echo "def expected : List String := [$SCALAR_OLEANS]" + cat <<'LEANGATE' + +run_cmd do + let dir : System.FilePath := "Proofs" + let mut errs : Array String := #[] + let mut nMod := 0 + for name in expected do + let p := dir / name + -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes + -- this gate vacuous for that module, which must be an error, not a skip. + unless (← p.pathExists) do + throwError "COVERAGE: {name} is in the manifest but its compiled artifact is absent" + nMod := nMod + 1 + let (mod, _) ← readModuleData p + for ci in mod.constants do + if ci matches .axiomInfo _ then + errs := errs.push s!" {name}: {ci.name}" + unless errs.isEmpty do + throwError "AXIOM DECLARED in the scalar layer:\n{String.intercalate "\n" errs.toList}" + logInfo s!" kernel confirms: {nMod} compiled scalar modules (the manifest, by membership), none declares an axiom" +LEANGATE +} > "$GATE" +cd "$AENEAS_LEAN" +GATE_RC=0 +lake env bash -c " + set -uo pipefail + cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" + cd '$HERE' + LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$GATE' +" || GATE_RC=$? +rm -f "$GATE" "${GATE%.lean}.olean" +[ "$GATE_RC" -eq 0 ] || { echo "SCALAR AXIOM GATE FAILED"; exit 1; } + +# ── Phase 2c: declaration inventory ───────────────────────────────────────── +# Until today these 13 modules were the only part of the proof corpus with no +# declaration inventory: check.sh Phase 2c covers the main chain and named them +# as uncovered on every run. This closes that. +echo "=== Phase 2c: scalar declaration inventory ===" +INVFAIL=0 +INVLOG=$(mktemp /tmp/check-scalar-inv-XXXX.log) cd "$AENEAS_LEAN" lake env bash -c " + set -uo pipefail + cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" + cd '$HERE' + LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=8192 '$HERE/lean-guard' Proofs/InventoryScalar.lean +" > "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "SCALAR INVENTORY COMPILE FAILED"; rm -f "$INVLOG"; exit 1; } +OBS=$(mktemp /tmp/check-scalar-obs-XXXX.log) +grep -E '^INV\|' "$INVLOG" > "$OBS" +grep '^INV-COUNT|' "$INVLOG" | tail -1 >> "$OBS" +"$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist-scalar.txt" || INVFAIL=1 +rm -f "$INVLOG" "$OBS" +# The driver's corpus list must BE this script's manifest, both directions. +COVERED=$(grep -oE '`Proofs\.[A-Za-z0-9]+' "$HERE/Proofs/InventoryScalar.lean" | sed 's/`Proofs\.//' | sort -u) +for m in "${PROOFS[@]}"; do + grep -qx "$m" <<<"$COVERED" || { echo " UNINVENTORIED: $m is compiled here but the driver does not cover it"; INVFAIL=1; } +done +while read -r m; do + [ -z "$m" ] && continue + case " ${PROOFS[*]} " in (*" $m "*) ;; (*) echo " PHANTOM: driver claims $m, not in this manifest"; INVFAIL=1;; esac +done <<<"$COVERED" +[ "$INVFAIL" = 0 ] || { echo "SCALAR INVENTORY FAILED"; exit 1; } + +# ── Phase 3: per-certificate exact-cone audit ─────────────────────────────── +# Was: count the lines of #print axioms output that matched the clean cone and +# compare against 13. A count cannot say WHICH certificate is clean, and it +# passes just as happily if one certificate's cone is reported twice. Each +# certificate is now asserted by name. +echo "=== Phase 3: per-certificate exact-cone audit ===" +cd "$AENEAS_LEAN" +AUD_OUT=$(lake env bash -c " set -uo pipefail export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\" cd '$HERE' AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean') - { echo 'import Proofs.ScalarMain'; echo 'import Proofs.ScalarWideSpec'; echo 'import Proofs.ScalarUnpackSpec'; echo 'import Proofs.ScalarFromBytesSpec'; echo '#print axioms ScalarProofs.L_val' - echo '#print axioms ScalarProofs.sub_loop_spec' - echo '#print axioms ScalarProofs.sub_loop1_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; echo '#print axioms ScalarProofs.mul_internal_spec' - echo '#print axioms ScalarProofs.part1_spec'; echo '#print axioms ScalarProofs.montgomery_reduce_spec'; echo '#print axioms ScalarProofs.mul_spec'; echo '#print axioms ScalarProofs.scalarImplementation'; echo '#print axioms ScalarProofs.montgomery_mul_spec'; echo '#print axioms ScalarProofs.bytes_unpack_spec'; echo '#print axioms ScalarProofs.from_bytes_wide_spec'; } > \"\$AUD\" - OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1) - echo \"\$OUT\" + { echo 'import Proofs.ScalarFromBytesSpec'; echo 'import Proofs.ScalarMain'; echo 'import Proofs.ScalarUnpackSpec'; echo 'import Proofs.ScalarWideSpec' + for c in ${CERTS[*]}; do echo \"#print axioms \$c\"; done; } > \"\$AUD\" + OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1) rm -f \"\$AUD\" \"\${AUD%.lean}.olean\" - N=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || true) - [ \"\$N\" -eq 13 ] || { echo \"AXIOM AUDIT FAILED: \$N/13 clean\"; exit 1; } -" || { echo FAIL; exit 1; } -echo " L_val axiom-clean" + echo \"\$OUT\" +") || { echo "$AUD_OUT"; echo "SCALAR AUDIT COMPILE FAILED"; exit 1; } +FLAT=$(tr '\n' ' ' <<<"$AUD_OUT" | tr -s ' ') +AUDFAIL=0 +for c in "${CERTS[@]}"; do + grep -qF "'$c' depends on axioms: $EXPECTED" <<<"$FLAT" \ + || { echo " NOT CLEAN or NOT FOUND: $c"; AUDFAIL=1; } +done +if [ "$AUDFAIL" != 0 ]; then + echo "SCALAR AXIOM AUDIT FAILED"; echo "$AUD_OUT" | tail -20 | sed 's/^/ /'; exit 1 +fi +echo " ${#CERTS[@]}/${#CERTS[@]} scalar certificates report exactly $EXPECTED" echo "" -echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round through RR) proven mod ℓ; aggregate certificate scalarImplementation kernel-audited." +echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round" +echo "through RR) proven mod ℓ; aggregate certificate scalarImplementation" +echo "kernel-audited; declaration surface inventoried; harness pinned." diff --git a/verification/check.sh b/verification/check.sh index f2e8abc..24cd83c 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -208,8 +208,10 @@ HARNESS_EXTRA=( AUDIT-MANIFEST.txt # the statement block Phase 3c's digest is taken over GEN-MODEL.sha256 # the extracted-model pins Phase 0b enforces inventory-allowlist.txt # the audit surface Phase 2c diffs against + inventory-allowlist-scalar.txt # the scalar layer's audit surface (second button) Proofs/Audit.lean # the audit driver: it computes the digest it is judged by Proofs/InventoryCore.lean # inventory machinery + Proofs/InventoryScalar.lean # inventory driver: the scalar layer Proofs/Inventory.lean # inventory driver: main chain ) echo "=== Phase 0c: harness integrity ===" @@ -251,6 +253,51 @@ if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lea fi echo " clean: no trivial stubs, no True targets, no axioms outside gen/" +# ── Phase 1b: the two-button seam ─────────────────────────────────────────── +# WHY. This repository is checked by TWO buttons: this script covers the field, +# curve and signature layers, and check-scalar.sh covers the scalar layer. +# Until 2026-07-30 neither asserted anything about the other's scope, and this +# script's dead-file gate simply SKIPPED anything named Scalar*. A new +# Proofs/ScalarX.lean was therefore gated by nothing at all: absent from this +# manifest by exemption, absent from the other by omission, compiled by +# neither, inventoried by neither. +# +# The fix is mutual: each button reads the OTHER's manifest and asserts that +# every shipped proof source belongs to exactly one of them. Both directions, +# so a file can neither fall between the two nor be claimed by both. +echo "=== Phase 1b: two-button seam ===" +SEAMFAIL=0 +SCALAR_SH="$HERE/check-scalar.sh" +if [ ! -f "$SCALAR_SH" ]; then + echo " FATAL: check-scalar.sh is absent — half the corpus would go unchecked." + exit 1 +fi +SCALAR_MANIFEST=$(grep -m1 '^PROOFS=(' "$SCALAR_SH" | sed 's/^PROOFS=(//; s/).*$//' | tr ' ' '\n' | sed '/^$/d' | sort -u) +if [ -z "$SCALAR_MANIFEST" ]; then + echo " FATAL: could not read check-scalar.sh's manifest; refusing to guess its scope." + exit 1 +fi +MAIN_MANIFEST=$(printf '%s\n' "${PROOFS[@]}" | sort -u) +# 1. Every shipped proof source belongs to exactly one manifest. +for f in "$HERE"/Proofs/*.lean; do + b=$(basename "$f" .lean) + case "$b" in AxiomCheck|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac + inm=0; ins=0 + grep -qx "$b" <<<"$MAIN_MANIFEST" && inm=1 + grep -qx "$b" <<<"$SCALAR_MANIFEST" && ins=1 + if [ $((inm + ins)) -eq 0 ]; then + echo " ORPHAN: Proofs/$b.lean is in NEITHER manifest — compiled and audited by no button"; SEAMFAIL=1 + elif [ $((inm + ins)) -eq 2 ]; then + echo " DOUBLE-CLAIMED: Proofs/$b.lean is in BOTH manifests — the buttons disagree about scope"; SEAMFAIL=1 + fi +done +# 2. Neither manifest may name a file that does not exist. +while read -r m; do + [ -z "$m" ] && continue + [ -f "$HERE/Proofs/$m.lean" ] || { echo " PHANTOM: check-scalar.sh lists $m, which does not exist"; SEAMFAIL=1; } +done <<<"$SCALAR_MANIFEST" +[ "$SEAMFAIL" = 0 ] && echo " every proof source belongs to exactly one button ($(grep -c . <<<"$MAIN_MANIFEST") here, $(grep -c . <<<"$SCALAR_MANIFEST") scalar)" +[ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; } # ── Phase 2: compile everything shipped ───────────────────────────────────── echo "=== Phase 2: compile ===" LOG=$(mktemp /tmp/check-compile-XXXX.log) @@ -276,7 +323,7 @@ lake env bash -c " # with the corpus already in the environment, and the two of them cannot be # imported together. They are NOT unchecked — Phase 2b reads their compiled # .olean like every other module, and Phase 0c pins their sources. - case \"\$b\" in Inventory|InventoryBasic|InventoryCore) continue;; esac + case \"\$b\" in Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac case \"\$b\" in Scalar*) continue;; esac # scalar layer: checked by check-scalar.sh (coherence pass 2) case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f not in check manifest\"; exit 1;; esac done @@ -393,7 +440,10 @@ cd "$AENEAS_LEAN" # Proofs.ConstSpecs; risc0 and betrusted have no Proofs.Basic at all). A # hardcoded pair would silently look for a file that does not exist here. DRIVERS=$(ls "$HERE"/Proofs/Inventory*.lean 2>/dev/null | xargs -r -n1 basename \ - | sed 's/\.lean$//' | grep -v '^InventoryCore$' | sort) + | sed 's/\.lean$//' | grep -vE '^(InventoryCore|InventoryScalar)$' | sort) +# InventoryScalar belongs to check-scalar.sh, which compiles the modules it +# covers. Globbing Inventory*.lean swept it in here, after which this phase +# correctly complained that its own manifest lacks the scalar modules. if [ -z "$DRIVERS" ]; then echo " NO INVENTORY DRIVER FOUND — the audit surface would go unchecked."; exit 1 fi @@ -437,7 +487,7 @@ while read -r m; do done <<<"$COVERED" for f in "$HERE"/Proofs/*.lean; do b=$(basename "$f" .lean) - case "$b" in Audit|Inventory|InventoryBasic|InventoryCore) continue;; esac + case "$b" in Audit|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac grep -qx "$b" <<<"$COVERED" || echo " NOT INVENTORIED HERE (separate button): Proofs/$b.lean" done [ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; } diff --git a/verification/inventory-allowlist-scalar.txt b/verification/inventory-allowlist-scalar.txt new file mode 100644 index 0000000..b533240 --- /dev/null +++ b/verification/inventory-allowlist-scalar.txt @@ -0,0 +1,1894 @@ +# inventory-allowlist-scalar.txt — the pinned audit surface of the SCALAR layer +# (check-scalar.sh Phase 2c). Same format and same discipline as the main +# allowlist: INV|module|name|kind|cone, one line per constant, reviewed as a +# DIFF rather than read line by line. +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_18|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_20|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_22|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_23|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_25|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_26|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_34|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_36|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_46|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_54|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_61|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_62|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_65|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_69|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_70|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_71|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_72|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_73|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_74|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._proof_1_75|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_4|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_60|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_6|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec._simp_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_loop_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._proof_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._proof_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._proof_1_18|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._proof_1_20|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_2|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_4|theorem|Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_8|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarAddSpec|ScalarProofs.add_val_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarAddSpec|_private.Proofs.ScalarAddSpec.0.ScalarProofs.loop_step.match_1.eq_1|theorem| +INV|Proofs.ScalarAddSpec|_private.Proofs.ScalarAddSpec.0.ScalarProofs.loop_step.match_1.eq_2|theorem| +INV|Proofs.ScalarAddSpec|_private.Proofs.ScalarAddSpec.0.ScalarProofs.loop_step.match_1.splitter|def| +INV|Proofs.ScalarAddSpec|_private.Proofs.ScalarAddSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_1|theorem| +INV|Proofs.ScalarAddSpec|_private.Proofs.ScalarAddSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_2|theorem| +INV|Proofs.ScalarAddSpec|_private.Proofs.ScalarAddSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.splitter|def| +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_31|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_36|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_40|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_43|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_54|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_60|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_0|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_31|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_33|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_34|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_36|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_43|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_46|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_57|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_43|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_46|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_57|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_57|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_62|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_65|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_62|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_65|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_62|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_65|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_10|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_16|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_17|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_spec_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_48|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_65|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_67|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_69|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_71|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0._simp_1_72|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_0|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_33|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_34|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_36|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_37|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_39|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_48|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_65|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_67|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_69|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_71|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1._simp_1_72|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_44|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_47|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_49|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_54|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_57|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_70|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2._simp_1_71|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_44|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_47|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_49|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_54|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_57|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_70|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3._simp_1_71|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_48|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_70|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4._simp_1_71|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_48|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_70|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5._simp_1_71|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_48|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_70|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6._simp_1_71|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_1|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_44|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_47|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_49|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_70|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_12|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_14|theorem|Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_18|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_19|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_20|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_21|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_22|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_23|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_24|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_25|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7._simp_1_71|theorem|propext +INV|Proofs.ScalarBytesSpec|ScalarProofs.bytes_word_loop_tail_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarBytesSpec|_private.Proofs.ScalarBytesSpec.0.ScalarProofs.loop_step.match_1.eq_1|theorem| +INV|Proofs.ScalarBytesSpec|_private.Proofs.ScalarBytesSpec.0.ScalarProofs.loop_step.match_1.eq_2|theorem| +INV|Proofs.ScalarBytesSpec|_private.Proofs.ScalarBytesSpec.0.ScalarProofs.loop_step.match_1.splitter|def| +INV|Proofs.ScalarBytesSpec|_private.Proofs.ScalarBytesSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_1|theorem| +INV|Proofs.ScalarBytesSpec|_private.Proofs.ScalarBytesSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_2|theorem| +INV|Proofs.ScalarBytesSpec|_private.Proofs.ScalarBytesSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.splitter|def| +INV|Proofs.ScalarDenote|ScalarProofs.Ell|def| +INV|Proofs.ScalarDenote|ScalarProofs.L_bnd|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.L_limbs|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.L_val|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.Sc.exists_limbs.match_1_1|def|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.Sc.exists_limbs|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.ScBnd|def|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.Sc|def|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs._aux_Proofs_ScalarDenote___unexpand_ScalarProofs_scDenote_1|def| +INV|Proofs.ScalarDenote|ScalarProofs.scDenote|def|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.scLimbs|def|propext +INV|Proofs.ScalarDenote|ScalarProofs.scVal._sparseCasesOn_1|def|propext +INV|Proofs.ScalarDenote|ScalarProofs.scVal._sparseCasesOn_2|def|propext +INV|Proofs.ScalarDenote|ScalarProofs.scVal.match_1|def|propext +INV|Proofs.ScalarDenote|ScalarProofs.scVal_eq|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.scVal|def|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarDenote|ScalarProofs.«_aux_Proofs_ScalarDenote___macroRules_ScalarProofs_term⟦_⟧_1»|def| +INV|Proofs.ScalarDenote|ScalarProofs.«term⟦_⟧»|def| +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_3|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_7|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_8|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.fbw_parts_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_11|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_12|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_18|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_19|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_20|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_21|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_22|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec._simp_1_9|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.from_bytes_wide_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_1|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_32|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_35|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_11|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_12|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_13|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_18|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_19|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_20|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_21|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_22|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_23|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec._simp_1_24|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_hi_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_1|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_32|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_35|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_39|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_11|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_12|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_13|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_18|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_19|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_20|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_21|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_22|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_23|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec._simp_1_24|theorem|propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.split_words_lo_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.wide_split_telescope._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarFromBytesSpec|ScalarProofs.wide_split_telescope|theorem|Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.RR_denote|theorem|Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.RR_limbs|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.RR_lt|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.RR_scVal|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.R_isUnit|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.col_bound|theorem|Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_12|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_13|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_14|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_18|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarFullMulSpec|ScalarProofs.mul_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarLoop|Aeneas.Std.core.cmp.impls.PartialOrdUsize.lt.eq_1|theorem| +INV|Proofs.ScalarLoop|Aeneas.Std.core.iter.range.StepUsize.forward_checked.eq_1|theorem|propext +INV|Proofs.ScalarLoop|ScalarProofs.loop_step.match_1|def| +INV|Proofs.ScalarLoop|ScalarProofs.loop_step|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarLoop|ScalarProofs.range_next_ge_spec._proof_1_4|theorem|Quot.sound,propext +INV|Proofs.ScalarLoop|ScalarProofs.range_next_ge_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarLoop|ScalarProofs.range_next_lt_spec._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarLoop|ScalarProofs.range_next_lt_spec._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarLoop|ScalarProofs.range_next_lt_spec._simp_1_6|theorem|propext +INV|Proofs.ScalarLoop|ScalarProofs.range_next_lt_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarLoop|_private.Proofs.ScalarLoop.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.ScalarLoop|_private.Proofs.ScalarLoop.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.ScalarLoop|_private.Proofs.ScalarLoop.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.ScalarMain|ScalarProofs.canonical_mul_bound|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMain|ScalarProofs.scalarImplementation|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMain|ScalarProofs.scalar_add_correct|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMain|ScalarProofs.scalar_mul_correct|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMain|ScalarProofs.scalar_sub_correct._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMain|ScalarProofs.scalar_sub_correct._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMain|ScalarProofs.scalar_sub_correct|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|Aeneas.Std.Array.make.congr_simp|theorem| +INV|Proofs.ScalarMontSpec|Aeneas.Std.Array.make.eq_1|theorem| +INV|Proofs.ScalarMontSpec|ScalarProofs.LFACTOR_val|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_bound._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_bound|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_cancel|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_head_telescope|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_key|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_18|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_20|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_21|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_22|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_23|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_24|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_25|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_26|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_27|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_28|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_32|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_34|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_35|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_37|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_39|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_40|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_43|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_44|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_46|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_47|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_49|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_51|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_54|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_3|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_5|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.mont_tail_telescope|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_15|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_18|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_20|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._proof_1_22|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_3|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_7|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_8|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part1_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._proof_1_15|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._proof_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._proof_1_18|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_3|theorem|Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_7|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_8|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarMontSpec|ScalarProofs.part2_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._proof_1_15|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._proof_1_16|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._proof_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_3|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_7|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_8|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.m_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_18|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_20|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_21|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_22|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_23|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_26|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_27|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_28|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_32|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_34|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_35|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_37|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_39|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_40|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_41|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_43|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_44|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_46|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_47|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_49|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_51|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_54|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_55|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_57|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_58|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_59|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_60|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_61|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_2|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_4|theorem|Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_8|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarMulSpec|ScalarProofs.mul_internal_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_16|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_17|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_18|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_20|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_22|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_23|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_25|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_26|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_28|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_32|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_33|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_35|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_36|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_38|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_39|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_40|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_41|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_43|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_45|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_46|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_47|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_48|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_49|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_51|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_54|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_56|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_57|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_60|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_62|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_65|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_67|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_69|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._proof_1_70|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_2|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_4|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_8|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.montgomery_reduce_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.nonce_sum_bound._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarReduceSpec|ScalarProofs.nonce_sum_bound|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|Aeneas.Std.I32.ofInt.congr_simp|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.ZERO_limbs|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.add_telescope._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.add_telescope|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.nat_and_mask52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.nat_and_mask64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.nat_shift52|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.nat_shift63|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.scDenote.eq_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_22|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_23|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_30|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_32|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_33|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_36|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_40|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_52|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_53|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_60|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_61|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_67|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_69|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_70|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_72|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_73|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_74|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_75|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_76|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_77|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_78|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_79|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_80|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_81|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_82|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_83|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_84|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_85|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._proof_1_86|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_12|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_18|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_19|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_20|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_71|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_7|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec._simp_1_9|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_one_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_22|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_23|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_26|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_29|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_31|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_33|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_34|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_36|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_39|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_40|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_41|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_42|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_46|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_48|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_50|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_51|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_55|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_57|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_58|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_60|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_61|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_62|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_63|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_64|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_66|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_67|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_68|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_69|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_71|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_72|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_73|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_75|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_76|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_77|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_78|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._proof_1_79|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_12|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_18|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_19|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_20|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_74|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_7|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec._simp_1_9|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop1_zero_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_22|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_23|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_31|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_32|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_33|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_35|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_36|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_37|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_38|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_39|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_40|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_42|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_43|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_44|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_45|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_46|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_47|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_49|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_50|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_51|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_52|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_53|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_54|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_56|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_58|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_59|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_60|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_61|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_62|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_63|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_64|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_65|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_66|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_67|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_68|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_69|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_70|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_71|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_72|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_73|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_74|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_75|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_76|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_77|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._proof_1_78|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_11|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_12|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_18|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_19|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_20|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_57|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_7|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec._simp_1_9|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_loop_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_step_arith._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_step_arith._proof_1_2|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_step_arith|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_telescope._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_telescope|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_17|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_18|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_19|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_20|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_22|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_23|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_24|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_28|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_30|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_10|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_3|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_5|theorem|Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec._simp_1_9|theorem|propext +INV|Proofs.ScalarSubSpec|ScalarProofs.sub_val_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|_private.Proofs.ScalarSubSpec.0.ScalarProofs.loop_step.match_1.eq_1|theorem| +INV|Proofs.ScalarSubSpec|_private.Proofs.ScalarSubSpec.0.ScalarProofs.loop_step.match_1.eq_2|theorem| +INV|Proofs.ScalarSubSpec|_private.Proofs.ScalarSubSpec.0.ScalarProofs.loop_step.match_1.splitter|def| +INV|Proofs.ScalarSubSpec|_private.Proofs.ScalarSubSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_1|theorem| +INV|Proofs.ScalarSubSpec|_private.Proofs.ScalarSubSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_2|theorem| +INV|Proofs.ScalarSubSpec|_private.Proofs.ScalarSubSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.splitter|def| +INV|Proofs.ScalarSubSpec|curve25519_dalek.backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut.eq_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarSubSpec|curve25519_dalek.backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index.eq_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_19|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_21|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_23|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_25|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_27|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_29|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_31|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_33|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_10|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_11|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_12|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_13|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_14|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_15|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_16|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_17|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_18|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_35|theorem|propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_5|theorem|Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_7|theorem|Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec._simp_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|ScalarProofs.bytes_unpack_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarUnpackSpec|_private.Proofs.ScalarUnpackSpec.0.ScalarProofs.loop_step.match_1.eq_1|theorem| +INV|Proofs.ScalarUnpackSpec|_private.Proofs.ScalarUnpackSpec.0.ScalarProofs.loop_step.match_1.eq_2|theorem| +INV|Proofs.ScalarUnpackSpec|_private.Proofs.ScalarUnpackSpec.0.ScalarProofs.loop_step.match_1.splitter|def| +INV|Proofs.ScalarUnpackSpec|_private.Proofs.ScalarUnpackSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_1|theorem| +INV|Proofs.ScalarUnpackSpec|_private.Proofs.ScalarUnpackSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.eq_2|theorem| +INV|Proofs.ScalarUnpackSpec|_private.Proofs.ScalarUnpackSpec.0.curve25519_dalek.backend.serial.u64.field.FieldElement51.square2_loop.body.match_1.splitter|def| +INV|Proofs.ScalarWideSpec|ScalarProofs.R_bnd|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.R_denote|theorem|Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.R_limbs|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.R_lt|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.R_scVal|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_3|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_4|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_5|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_6|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_7|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_9|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec|theorem|Classical.choice,Quot.sound,propext