Theorem: get'_cons_succ (Saturn/Vector.lean)

State before:
α : Type
n : ℕ
x : α
ys : Vector α n
i : ℕ
iw : i < n
⊢ get' (x ::ᵥ ys) (i + 1) (_ : succ (i + 1) ≤ succ n) = get' ys i iw
Tactic:
rfl
State after:
no goals