proof(SafeUrl): DISCHARGE appendAssociative via Data.List.Equalities (proven#90 #107 #119) (#128)

\`\`\`idris
appendAssociative qs1 qs2 qs3 = Data.List.Equalities.appendAssociative
qs1 qs2 qs3
\`\`\`

\`appendQueryStrings = (++)\` (Query.idr L205-206), so the goal reduces
to standard list append-associativity. Discharged via contrib's
\`Data.List.Equalities.appendAssociative\` (already imported here via
#97).

The OWED comment said this was "stdlib-plumbing, not a fundamental gap"
— confirmed.

Refs #90 #107 #119

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

Author: hyperpolymath

src/Proven/SafeUrl/Proofs.idr

@@ -257,13 +257,16 @@ export
 ||| `Data.List` not exposing `appendAssociative` as a `%reducible`
 ||| rewrite (the proof exists in Prelude but requires induction on
 ||| `qs1`, and `Refl` cannot close it for abstract `qs1`). Discharge
-||| by importing `Data.List.appendAssociative` and rewriting (the
-||| proof is in-Idris2 — this is a stdlib-plumbing OWED, not a
-||| fundamental gap).
-export
-0 appendAssociative : (qs1, qs2, qs3 : QueryString) ->
-                      appendQueryStrings (appendQueryStrings qs1 qs2) qs3 =
-                      appendQueryStrings qs1 (appendQueryStrings qs2 qs3)
+||| DISCHARGED via `Data.List.Equalities.appendAssociative` from
+||| contrib. `appendQueryStrings = (++)` (Query.idr L205-206), so the
+||| goal reduces to `(qs1 ++ qs2) ++ qs3 = qs1 ++ (qs2 ++ qs3)` —
+||| exactly the stdlib lemma. The OWED was a stdlib-plumbing residual,
+||| not a fundamental gap, as the comment noted.
+public export
+appendAssociative : (qs1, qs2, qs3 : QueryString) ->
+                    appendQueryStrings (appendQueryStrings qs1 qs2) qs3 =
+                    appendQueryStrings qs1 (appendQueryStrings qs2 qs3)
+appendAssociative qs1 qs2 qs3 = Data.List.Equalities.appendAssociative qs1 qs2 qs3
 
 --------------------------------------------------------------------------------
 -- URL Security Properties