Theorem: WType.elimL_mk (Logic/Vorspiel/W.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
γ : Type u_3
f : α → List γ → γ
a : α
v : β a → WType β
⊢ elimL f (mk a v) = f a (List.ofFn (fintypeArrowEquivFinArrow fun b => elimL f (v b)))
Tactic:
simp[elimL, elim]
State after:
no goals