Theorem: Primrec₂.of_equiv_iff'2 (Logic/Vorspiel/Computability.lean)

State before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β✝ : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β✝
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
β : Type u_8
e : β ≃ α₂
f : α₁ → β → σ
this : Primcodable β := Primcodable.ofEquiv α₂ e
h : Primrec₂ fun a b => f a (e.symm b)
⊢ ∀ (n : α₁ × β), f n.1 (e.symm (e n.2)) = f n.1 n.2
Tactic:
simp
State after:
no goals