by_cases hx : x < n <;> simp[hx]
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if x < n then x + 1 else 0) = encode (if hx : x < n then some ⟨x, hx⟩ else none)
case pos
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
hx : x < n
⊢ x = encode ⟨x, ⋯⟩