fix(abi): remove duplicate allTake in Boj.SafetyLemmas (core proofs green) (#237)

Fixes the pre-existing Idris2 failure surfaced on #234/#236 (not caused
by either — they just triggered the path-gated Idris2 job by touching a
`.idr`).

## Root cause
`allTake` was defined **twice** in `src/abi/Boj/SafetyLemmas.idr`:
- lines ~122–130 — `{p} -> {n} -> {xs} -> allRec p xs = True -> allRec p
(take n xs) = True`
- lines ~213–221 — same lemma, implicit args in a different order (`{p}
-> {xs} -> {n}`)

→ `Error: Boj.SafetyLemmas.allTake is already defined` → the **core ABI
package `boj.ipkg` failed** type-check (`PASS=104 FAIL=1`). It was
masked normally because the Idris2 job is path-gated and skips unless a
`.idr` changes.

## Fix
Kept the **first** definition — a complete, **total** proof (no
`postulate`, no `believe_me`) — and removed the redundant second copy.
No proof is weakened or stubbed.

Both callers use inferred implicits, so the removed copy's argument
order didn't matter to them:
- `Boj/SafePromptInjection.idr:168` — `MkDelimiterCharsafe (take n cs)
{prf = allTake prf}`
- `Boj/SafeHTTP.idr:139` — `MkHeaderCharsafe (take n cs) {prf = allTake
prf}`

## Verification
Expected: `scripts/typecheck-proofs.sh` → **PASS=105 FAIL=0**. Idris2
isn't available in the authoring environment, so the **Idris2 type-check
CI job is the proof verification** here — it should go from failing to
green on this PR (and this is the first PR that *should* pass it cleanly
when the job runs).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---
_Generated by [Claude
Code](https://claude.ai/code/session_01XrPAh7eBSUcVKauTVdXH9Y)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

src/abi/Boj/SafetyLemmas.idr

@@ -210,16 +210,6 @@ allNotImpliesAnyFalse {p} {xs = x :: xs'} prf with (p x) proof pEq
   allNotImpliesAnyFalse {p} {xs = x :: xs'} prf | False =
     allNotImpliesAnyFalse {xs = xs'} prf
 
-||| If `allRec p xs = True`, then `allRec p (take n xs) = True`.
-export
-allTake : {p : a -> Bool} -> {xs : List a} -> {n : Nat} ->
-          allRec p xs = True -> allRec p (take n xs) = True
-allTake {n = Z} _ = Refl
-allTake {xs = []} {n = S _} _ = Refl
-allTake {p} {xs = x :: xs'} {n = S n'} prf with (p x) proof eq
-  allTake {p} {xs = x :: xs'} {n = S n'} prf | True  = allTake {xs = xs'} {n = n'} prf
-  allTake {p} {xs = x :: xs'} {n = S n'} prf | False = absurd prf
-
 ||| Convert a Bool lte witness to LTE.
 export
 fromLteTrue : (a, b : Nat) -> (a <= b) = True -> LTE a b