Theorem: Qq.eq_cons_app_succ_of_eq (Logic/Vorspiel/Meta.lean)

State before:
n : ℕ
α : Type u
a b : α
as : Fin n → α
i : Fin n
has : as i = b
⊢ (a :> as) i.succ = b
Tactic:
simp[has]
State after:
no goals