Theorem: Primrec.casesOn_eq_uncurry (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 τ
l : σ → List α
f : σ → β
g : σ → α → List α → β
⊢ (fun x => List.casesOn (l x) (f x) (g x)) = fun x =>
    List.casesOn (l x) (f x) fun a as => Function.uncurry (g x) (a, as)
Tactic:
rfl
State after:
no goals