exact this.comp Primrec.id (Primrec₂.pair.comp hg hw)
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
this : Primrec₂ fun z p => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) p.1 p.2
⊢ Primrec fun z => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (g z) (w z)
no goals