no goals
c₁ c₂ : Code
n₁ n₂ : ℕ
h : curry c₁ n₁ = curry c₂ n₂
⊢ c₁ = c₂
injection h
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : pair (Code.const n₁) Code.id = pair (Code.const n₂) Code.id
⊢ n₁ = n₂
c₁ c₂ : Code
n₁ n₂ : ℕ
h : curry c₁ n₁ = curry c₂ n₂
⊢ n₁ = n₂
injection h with h₁ h₂
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : pair (Code.const n₁) Code.id = pair (Code.const n₂) Code.id
⊢ n₁ = n₂
injection h₂ with h₃ h₄
no goals
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂
exact const_inj h₃