proof(model): close equivSym via Data.Bool.andCommutative (1/5 Cat B holes) (#123)

The two `all`-predicates inside `equiv` are conjoined; the reverse-
direction goal is the same conjunction commuted, so a single rewrite
by `andCommutative` collapses it to the premise. No primitive
String/Bits8 `==` reflexivity needed — pure boolean algebra over the
already-evaluated predicate values.

Verified locally: 4/4 modules build clean with `--total`.

Cat-B reclassification finding (see follow-up to #119):
- `equivSym`        — closed here (pure boolean algebra)
- `equivRefl`       — BLOCKED on primitive String/Bits8 `==` reflexivity
- `equivTrans`      — BLOCKED on `elem`-transitivity through filtered lists
- `undoRedoIdentity`     — non-theorem under propositional `=` (needs `equiv`)
- `undoRedoComposition`  — same as undoRedoIdentity
- `cnoWriteSameContent`  — body needs equiv-membership lemma chain
  (also blocked on primitive eq reflexivity at the leaves)

So 1/5 closeable purely; remaining 4 need a Q4-style decision
(axiom vs equiv-restate vs DecEq-rewrite of equiv).

Refs:
- valence-shell#119 — proof-hole inventory (Cat B)
- memory: reference_idris2_0_8_0_reserved_keywords.md

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

Author: hyperpolymath

proofs/idris2/src/Filesystem/Model.idr

@@ -8,6 +8,7 @@
 
 module Filesystem.Model
 
+import Data.Bool
 import Data.List
 import Data.Maybe
 import Data.String
@@ -214,12 +215,25 @@ export
 equivRefl : (fs : Filesystem) -> equiv fs fs = True
 equivRefl (MkFS entries) = ?equivReflProof
 
-||| Symmetry of equivalence
+||| Symmetry of equivalence.
+|||
+||| Closed via `Data.Bool.andCommutative` from Idris2 0.8.0's base
+||| stdlib. The two `all`-predicates inside `equiv` are conjoined; the
+||| reverse-direction goal is the same conjunction commuted, so a
+||| single rewrite by `andCommutative` collapses it to the premise.
+|||
+||| Does NOT need primitive String/Bits8 `==` reflexivity — this is
+||| pure boolean algebra over the already-evaluated predicate values.
+||| Contrast with `equivRefl` / `equivTrans`, which DO require leaf-
+||| level eq-reflexivity (tracked separately under issue #119).
 export
 equivSym : (fs1, fs2 : Filesystem) ->
            equiv fs1 fs2 = True ->
            equiv fs2 fs1 = True
-equivSym (MkFS e1) (MkFS e2) prf = ?equivSymProof
+equivSym (MkFS e1) (MkFS e2) prf =
+  rewrite andCommutative (all (\e => elem e e1) e2)
+                         (all (\e => elem e e2) e1)
+  in prf
 
 ||| Transitivity of equivalence
 export