fix(proofs): fix all remaining idris2 + Agda scope errors

ProverKindInjectivity.idr:
- Replace all 107 LTESucc towers with lteLit calls (eliminates off-by-one
  bug class permanently; Nunchaku was -1 close and Faial was +1)
- Add `import NatLte` for the machine-checked LTE helper
- Fix docstring range [0, 104] -> [0, 106] to match actual max discriminant

DispatchCorrectness.idr:
- Remove `import EchidnaABI.Provers` (pulls in a conflicting `proverLogic`
  from InteractiveAssistants; file only needs EchidnaABI.Types)
- Allows file to type-check with the echidnaabi package installed

proofs/agda/Basic.agda:
- Hoist `data ℕ` and `data _≡_` to module scope (were only in `where`
  blocks, causing scope errors when used in type signatures)
- Remove duplicate `data _≡_` from CombinatorLaws/CurryUncurryLaws
  (they now inherit from module scope)
- Instantiate SKK's second const with {B = A} to resolve unsolved meta

All 11 verification/proofs/idris2/ files now pass `idris2 --check`.
12/13 proofs/agda/ files pass (DispatchOrdering needs stdlib 2.1).

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

Author: claude

proofs/agda/Basic.agda

@@ -8,6 +8,17 @@
 
 module Basic where
 
+-- Propositional equality at module scope (used by trans-assoc, id-left, id-right)
+data _≡_ {A : Set} (x : A) : A → Set where
+  refl : x ≡ x
+
+infix 4 _≡_
+
+-- Natural numbers at module scope (used by id-nat)
+data ℕ : Set where
+  zero : ℕ
+  suc  : ℕ → ℕ
+
 --------------------------------------------------------------------------------
 -- Identity Proof
 --------------------------------------------------------------------------------
@@ -21,10 +32,6 @@ id x = x
 -- Example: identity for a specific type
 id-nat : (n : ℕ) → ℕ
 id-nat = id
-  where
-    data ℕ : Set where
-      zero : ℕ
-      suc  : ℕ → ℕ
 
 -- The identity function can also be written explicitly with a lambda
 id′ : {A : Set} → A → A
@@ -75,28 +82,14 @@ trans-assoc : {A B C D : Set}
             → (f : A → B) → (g : B → C) → (h : C → D)
             → (h ∘ (g ∘ f)) ≡ ((h ∘ g) ∘ f)
 trans-assoc f g h = refl
-  where
-    -- Propositional equality
-    data _≡_ {A : Set} (x : A) : A → Set where
-      refl : x ≡ x
-
-    infix 4 _≡_
 
 -- Proof that identity is a left identity for composition
 id-left : {A B : Set} → (f : A → B) → (id ∘ f) ≡ f
 id-left f = refl
-  where
-    data _≡_ {A : Set} (x : A) : A → Set where
-      refl : x ≡ x
-    infix 4 _≡_
 
 -- Proof that identity is a right identity for composition
 id-right : {A B : Set} → (f : A → B) → (f ∘ id) ≡ f
 id-right f = refl
-  where
-    data _≡_ {A : Set} (x : A) : A → Set where
-      refl : x ≡ x
-    infix 4 _≡_
 
 --------------------------------------------------------------------------------
 -- Additional Basic Combinators
@@ -125,13 +118,9 @@ infixr 0 _$_
 --------------------------------------------------------------------------------
 
 module CombinatorLaws where
-  data _≡_ {A : Set} (x : A) : A → Set where
-    refl : x ≡ x
-
-  infix 4 _≡_
-
   -- SKK = I (a famous combinator identity)
-  SKK : {A : Set} → (x : A) → S const const x ≡ id x
+  -- The second const needs B instantiated explicitly to resolve the implicit argument.
+  SKK : {A : Set} → (x : A) → S const (const {B = A}) x ≡ id x
   SKK x = refl
 
   -- Flip is involutive (applying it twice gets you back where you started)
@@ -164,9 +153,6 @@ uncurry f (x , y) = f x y
 
 -- Proof that curry and uncurry are inverses
 module CurryUncurryLaws where
-  data _≡_ {A : Set} (x : A) : A → Set where
-    refl : x ≡ x
-
   -- INTENTIONAL AXIOM: Function extensionality (funext)
   -- Justification: funext is consistent with Agda's type theory and is
   -- provable in Cubical Agda (--cubical). In plain Agda it must be

verification/proofs/idris2/DispatchCorrectness.idr

@@ -12,7 +12,6 @@
 module DispatchCorrectness
 
 import EchidnaABI.Types
-import EchidnaABI.Provers
 
 %default total