proof(SafeJson): fix appendLengthInc lengthSnoc arg order so the module compiles

Makes this branch type-check under a clean Idris2 0.8.0 + contrib
toolchain. `idris2 --check src/Proven/SafeJson/Proofs.idr` now builds all
five SafeJson modules (Core, Parser, Access, SafeJson, Proofs) with 0
errors (one pre-existing unreachable-clause warning in Access remains).

The two discharges this branch adds (anyMatchesTAny via 6-arm split,
singleKeyPath via with-pattern) are correct, but the module did not
compile because of a pre-existing bug carried in from #127:

  appendLengthInc used `lengthSnoc arr v`, but
  Data.List.Equalities.lengthSnoc is element-first (`lengthSnoc x xs`).
  Under Idris2 0.8.0 contrib this fails to type-check
  (Mismatch: JsonValue vs List ?a) and blocks the ENTIRE
  SafeJson.Proofs module, so none of its proofs were checkable.
  Corrected to `lengthSnoc v arr`.

This is the failure the PR description attributed to "a local contrib
quirk [that] does NOT reproduce in CI". It is not local: it reproduces
on a clean v0.8.0 install, which also means main's own
`idris2 --build proven.ipkg` currently fails at this module.

Also corrects two proof comments to match what the compiler actually
accepts and removes stale /tmp/ scratch-path references:
  - singleKeyPath: getPath/getSegment are `covering` (via the
    `%default covering` in SafeJson.Access), not total. That annotation
    does not block the clause-level reduction the proof relies on, so
    they are left covering and the proof still goes through (verified).
  - anyMatchesTAny: the six-arm split needs no totality change.

No believe_me / postulate / idris_crash / assert_total introduced.

Refs #127, proven#90 #107 #119.

https://claude.ai/code/session_01MN5vzRR4MK2dkDNaHqqRDy

Author: claude

src/Proven/SafeJson/Proofs.idr

@@ -198,14 +198,18 @@ prependLengthInc v arr = Refl
 ||| DISCHARGED: `append v (JsonArray arr) = JsonArray (arr ++ [v])`
 ||| (SafeJson.idr L233-234), so the goal reduces to
 ||| `Just (length (arr ++ [v])) = Just (length arr + 1)`. Apply
-||| `lengthSnoc arr v : length (arr ++ [v]) = S (length arr)`, then
+||| `lengthSnoc v arr : length (arr ++ [v]) = S (length arr)`, then
 ||| close the `S n` vs `n + 1` gap with `plusCommutative 1 n`.
+||| (`Data.List.Equalities.lengthSnoc` takes the element first, then the
+||| list — `lengthSnoc x xs`; the previous `lengthSnoc arr v` argument
+||| order did not type-check under Idris2 0.8.0 contrib and blocked the
+||| whole module from compiling.)
 public export
 appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) ->
                   arrayLength (append v (JsonArray arr)) =
                   Just (length arr + 1)
 appendLengthInc v arr =
-  cong Just (trans (lengthSnoc arr v) (plusCommutative 1 (length arr)))
+  cong Just (trans (lengthSnoc v arr) (plusCommutative 1 (length arr)))
 
 --------------------------------------------------------------------------------
 -- Path Access Properties
@@ -218,16 +222,15 @@ emptyPathIdentity v = Refl
 
 ||| DISCHARGED: a single-segment `Key k` path equals direct `lookup`:
 ||| `getPath [Key k] (JsonObject obj) = lookup k obj`.
-||| The OWED comment claimed `getPath`/`getSegment` are `covering`
-||| (which would block reduction), but inspection of the current
-||| `Proven.SafeJson.Access` source shows neither carries the
-||| annotation — they are total. Discharge proceeds:
-|||   getPath [Key k] (JsonObject obj)
-|||     = case getSegment (Key k) (JsonObject obj) of {Nothing => Nothing; Just v => getPath [] v}
-|||     = case lookup k obj of {Nothing => Nothing; Just v => Just v}
-||| `with`-pattern on `lookup k obj` discharges both arms by `Refl`
-||| (Maybe-identity). Empirically verified at
-||| `/tmp/charrefl/src/TestJsonPath.idr`.
+||| On the concrete spine `[Key k]` / `JsonObject obj`, `getPath` and
+||| `getSegment` reduce by clause-matching to
+|||   case lookup k obj of { Nothing => Nothing; Just v => Just v }
+||| Abstracting `lookup k obj` with a `with`-pattern then closes both
+||| arms by `Refl` (Maybe-identity).
+||| (`getPath`/`getSegment` are `covering` via the `%default covering`
+||| in `Proven.SafeJson.Access`; that annotation does not block this
+||| clause-level reduction, so they are left covering and the proof
+||| still goes through.)
 public export
 singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) ->
                 getPath [Key k] (JsonObject obj) = lookup k obj
@@ -327,14 +330,13 @@ stringMatchesTString s = Refl
 ||| DISCHARGED: every `JsonValue` matches `TAny`:
 ||| `matchesType v TAny = True` for all `v`.
 ||| Definitionally `matchesType _ TAny = True` (`SafeJson.idr` L353).
-||| The OWED comment claimed the covering-vs-total policy blocks
-||| reduction on an abstract `v`, but in practice the manual
-||| six-arm case-split it suggested (`JsonNull` / `JsonBool b` /
-||| `JsonNumber n` / `JsonString s` / `JsonArray arr` /
-||| `JsonObject pairs`) works: each concrete-constructor arm
-||| reduces through the catch-all `matchesType _ TAny = True`
-||| clause by `Refl`. Empirically verified at
-||| `/tmp/charrefl/src/TestJson.idr`.
+||| Discharged by a six-arm case-split on `v` (`JsonNull` / `JsonBool b`
+||| / `JsonNumber n` / `JsonString s` / `JsonArray arr` /
+||| `JsonObject pairs`): `matchesType _ TAny = True` is a catch-all, and
+||| for each concrete head every earlier clause demands a non-`TAny`
+||| second argument, so each arm reduces to the catch-all and closes by
+||| `Refl`. No totality change is needed — a concrete head per arm is
+||| sufficient even though `matchesType` is `covering`.
 public export
 anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True
 anyMatchesTAny JsonNull       = Refl