α : Type u
a : α
l : List α
⊢ (get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l
α : Type u
a : α
l : List α
⊢ ofFn (get (a :: l)) = a :: l
rw [ofFn_succ]
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => get (a :: l) (Fin.succ i)) = l
α : Type u
a : α
l : List α
⊢ (get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l
congr
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => get (a :: l) (Fin.succ i)) = l
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => get (a :: l) (Fin.succ i)) = l
simp only [Fin.val_succ]
no goals
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => get (a :: l) (Fin.succ i)) = l
exact ofFn_get l