n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (Vector.tail v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ (mOfFn fun i => (↑fun v => Vector.get v (Fin.succ i)) v) >>= f = f (Vector.tail v)
simp
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (ofFn (Vector.get (Vector.tail v)))
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (Vector.tail v)
rw [← ofFn_get v.tail]
case e_a.e_a
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ (fun i => Vector.get v (Fin.succ i)) = Vector.get (Vector.tail v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (ofFn (Vector.get (Vector.tail v)))
congr
case e_a.e_a.h
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
i : Fin n
⊢ Vector.get v (Fin.succ i) = Vector.get (Vector.tail v) i
case e_a.e_a
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ (fun i => Vector.get v (Fin.succ i)) = Vector.get (Vector.tail v)
funext i
no goals
case e_a.e_a.h
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
i : Fin n
⊢ Vector.get v (Fin.succ i) = Vector.get (Vector.tail v) i
simp