Theorem: Vec.append1_drop_last (Qpf/Util/Vec.lean)

State before:
α : Type u_1
n : ℕ
v : Vec α (n + 1)
i : Fin2 (Nat.succ n)
⊢ append1 (drop v) (last v) i = v i
Tactic:
cases i
State after:
case fz
α : Type u_1
n : ℕ
v : Vec α (n + 1)
⊢ append1 (drop v) (last v) Fin2.fz = v Fin2.fz

case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)

State before:
case fz
α : Type u_1
n : ℕ
v : Vec α (n + 1)
⊢ append1 (drop v) (last v) Fin2.fz = v Fin2.fz

case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)
Tactic:
rfl
State after:
case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)

State before:
case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)
Tactic:
rfl
State after:
no goals