Proof gate: core fails to typecheck (duplicate allTake) and CI typecheck job never runs Idris #343

Problem

The Idris core does not typecheck on main, and CI does not notice.

1. cd src/abi && idris2 --typecheck boj.ipkg fails with Error: Boj.SafetyLemmas.allTake is already defined. SafetyLemmas.idr has two allTake definitions, at about lines 146 and 237. They state the same lemma with the implicits in a different order. fix(abi): remove duplicate allTake in Boj.SafetyLemmas (core proofs green) #237 removed the duplicate, and merge 2a9a6c41 brought it back.
2. The proofs.yml job Idris2 type-check (core + all cartridge ABIs) fails before Idris runs, at asdf install idris2 "" (an empty version). That happened in runs 35570433668 (2026-09-21), 36389155371 (2026-09-28) and 37275630401 (2026-10-05).
3. On ordinary PRs and pushes to main the job is path-skipped, so the workflow reports success without checking anything (DEBT P-1).

Acceptance criteria

• Only one allTake remains in src/abi/Boj/SafetyLemmas.idr, and idris2 --typecheck boj.ipkg exits 0 locally on all 17 modules.
• The typecheck job installs a pinned Idris2 version (no empty asdf install argument) and reaches the typecheck step.
• bash scripts/check-trusted-base.sh still reports exactly 4 sanctioned axioms.
• The path-skip is removed from the typecheck and trusted-base jobs, or replaced with the always-run-plus-changes pattern from .claude/CLAUDE.md, so a broken core cannot show green.
• After the fix, README "What is proven" and site/index.html drop the "does not typecheck today" caveat.

Surfaced while preparing the Proven/Witnessed/Trusted ladder PR.