no goals
α : Type ?u.194459
β : Type u_1
σ : Type ?u.194465
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
this : Primcodable (List β) := prim H
l : List β
⊢ ∀ (r : List β), List.foldl (fun s b => b :: s) r l = List.reverseAux l r
induction l <;> simp [*, List.reverseAux]