v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x => Part.some [y]) (List.headI v) = Part.some [Nat.pred (List.headI v)]
v : List ℕ
⊢ eval pred v = pure [Nat.pred (List.headI v)]
simp [pred]
no goals
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x => Part.some [y]) (List.headI v) = Part.some [Nat.pred (List.headI v)]
cases v.headI <;> simp