no goals
x✝ : Code.const 0 = Code.const 0
⊢ 0 = 0
simp
n₁ n₂ : ℕ
h : comp succ (Code.const n₁) = comp succ (Code.const n₂)
⊢ n₁ + 1 = n₂ + 1
n₁ n₂ : ℕ
h : Code.const (n₁ + 1) = Code.const (n₂ + 1)
⊢ n₁ + 1 = n₂ + 1
dsimp [Nat.add_one, Nat.Partrec.Code.const] at h
n₁ n₂ : ℕ
h₁ : succ = succ
h₂ : Code.const n₁ = Code.const n₂
⊢ n₁ + 1 = n₂ + 1
n₁ n₂ : ℕ
h : comp succ (Code.const n₁) = comp succ (Code.const n₂)
⊢ n₁ + 1 = n₂ + 1
injection h with h₁ h₂
no goals
n₁ n₂ : ℕ
h₁ : succ = succ
h₂ : Code.const n₁ = Code.const n₂
⊢ n₁ + 1 = n₂ + 1
simp only [const_inj h₂]