no goals
α : Type u
β : Type v
γ : Type w
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ x = y
rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]
no goals
α : Type u
β : Type v
γ : Type w
x y : α
s t : Seq α
h : cons x s = cons y t
n : ℕ
⊢ get? s n = get? t n
simp_rw [← get?_cons_succ x s n, h, get?_cons_succ]