How does local completeness generalize to eliminators?

LocalProps.agda

{-
How does local completeness (http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf) generalize to eliminators?

Below is the eliminator for `ℕ` that does not include the inductive hypothesis `P n` in the `suc n` branch.
It still passes local completeness because the `suc n` branch still includes the `n` index, it merely omits the inductive hypothesis.

Caveats:
1. `ℕ` is a datatype rather than a standard logical proposition, and it has many proofs/inhabitants for the same type.
2. I'm being more strict here by requiring the expansion to equal the input, rather than merely proving the same proposition.
-}

open import Data.Nat
open import Relation.Binary.PropositionalEquality
module LocalProps where

caseℕ : ∀{ℓ} (P : ℕ → Set ℓ)
  (pz : P zero)
  (ps : (n : ℕ) {- → P n -} → P (suc n))
  → (n : ℕ) → P n
caseℕ P pz ps zero = pz
caseℕ P pz ps (suc n) = ps n {- (caseℕ P pz ps n) -}

completeness : (n : ℕ) → caseℕ (λ m → ℕ) zero (λ m → suc m) n ≡ n
completeness zero = refl
completeness (suc n) = refl

Reddit comments: http://www.reddit.com/r/dependent_types/comments/1akd80/how_does_local_completeness_identity_expansion/