Theorem: Primrec₂.of_equiv_iff (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 : σ → τ → β
⊢ (Primrec₂ fun a b => e (f a b)) ↔ Primrec₂ f
Tactic:
simp[Primrec₂, Primrec.of_equiv_iff]
State after:
no goals