English
Traversing a vector with the identity-pure applicative equals the identity on the vector.
Русский
Обход вектора через идентичную аппликативную чистую операцию равен идентичности на векторе.
LaTeX
$$$ \\text{traverse}_{Id}(x) = Id(x) $$$
Lean4
protected theorem id_traverse : ∀ x : Vector α n, x.traverse (pure : _ → Id _) = pure x :=
by
rintro ⟨x, rfl⟩; dsimp [Vector.traverse, cast]
induction x with
| nil => rfl
| cons x xs IH => simp! [IH]