proofs(idris2): close reverseConcat via Data.List.revAppend (#89 sub-marker) (#115)

Closes the parked `?reverseConcatProof` hole from PR #109 (Composition.idr).

The Idris2 0.8.0 stdlib provides:

    Data.List.revAppend :
      (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)

Which is exactly our claim, modulo direction of the equation. Applying
`sym` flips it to the conventional "concatenation distributes over
reverse" framing used by our local theorem:

    reverseConcat xs ys : reverse (xs ++ ys) = reverse ys ++ reverse xs
    reverseConcat xs ys = sym (revAppend xs ys)

The previous closed-form proof using induction + `rewrite` failed under
Idris2 0.8.0 because the stdlib's `reverse` is tail-recursive via
`reverseOnto`, and so does not structurally reduce per the Idris-1-style
expansion `reverse (x :: xs) = reverse xs ++ [x]`. Delegating to the
stdlib lemma is both shorter and more robust.

Verified locally with the full stacked context (#105 + #108 + #109 +
hardware-erase + audit-entry fixes + RMO overwriteIrreversible /
auditTrailCompleteness drive-bys for build progression). All 4 modules
build clean.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/idris2/src/Filesystem/Composition.idr

@@ -150,15 +150,17 @@ sequenceSplit (op :: ops1) ops2 fs =
   rewrite sequenceSplit ops1 ops2 (applyOp op fs) in Refl
 
 ||| Reverse of concatenation is concatenation of reverses (reversed).
-||| Body is a hole — Idris2 0.8.0's `reverse` definition does not reduce
-||| in the way the original closed-form proof assumed; needs a different
-||| approach (likely via `Data.List.reverseOntoSpec` or a helper lemma).
-||| Tracked under #89.
+||| Closes via `Data.List.revAppend` from Idris2 0.8.0's base stdlib.
+||| The stdlib lemma is stated with the equality symmetric to ours
+||| (`revAppend xs ys : reverse ys ++ reverse xs = reverse (xs ++ ys)`),
+||| so we apply `sym`. The local restatement keeps call sites stable
+||| and matches the conventional "concatenation distributes over
+||| reverse" framing.
 export
 reverseConcat :
   (xs, ys : List a) ->
   reverse (xs ++ ys) = reverse ys ++ reverse xs
-reverseConcat xs ys = ?reverseConcatProof
+reverseConcat xs ys = sym (revAppend xs ys)
 
 --------------------------------------------------------------------------------
 -- Undo/Redo Stack