Theorem: Vec.drop_append1' (Qpf/Util/Vec.lean)

State before:
α : Type u_1
n : ℕ
v : Vec α n
a : α
⊢ drop (append1 v a) = v
Tactic:
funext x
State after:
case h
α : Type u_1
n : ℕ
v : Vec α n
a : α
x : Fin2 n
⊢ drop (append1 v a) x = v x

State before:
case h
α : Type u_1
n : ℕ
v : Vec α n
a : α
x : Fin2 n
⊢ drop (append1 v a) x = v x
Tactic:
rfl
State after:
no goals