Theorem: WType.elimvL_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
γ : Type u_4
x : σ
fs : α → σ → σ
fγ : σ → α → List γ → γ
a : α
v : β a → WType β
⊢ elimvL fs fγ x (mk a v) = fγ x a (List.ofFn (fintypeArrowEquivFinArrow fun b => elimvL fs fγ (fs a x) (v b)))
Tactic:
simp[elimvL, elimv]
State after:
no goals