α : Type u_1
β : Type ?u.361685
γ : Type ?u.361688
σ : Type ?u.361691
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec fun a => a.fst :: Vector.toList a.snd
α : Type u_1
β : Type ?u.361685
γ : Type ?u.361688
σ : Type ?u.361691
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec fun a => Vector.toList (a.fst ::ᵥ a.snd)
simp
no goals
α : Type u_1
β : Type ?u.361685
γ : Type ?u.361688
σ : Type ?u.361691
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec fun a => a.fst :: Vector.toList a.snd
exact list_cons.comp fst (vector_toList_iff.2 snd)