Theorem: LoVe.length_listOfVec (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
α : Type
⊢ List.length (listOfVec Vec.nil) = 0
Tactic:
rfl
State after:
no goals

State before:
α : Type
a : α
n✝ : ℕ
v : Vec α n✝
⊢ List.length (listOfVec (Vec.cons a v)) = n✝ + 1
Tactic:
simp [listOfVec, length_listOfVec _ v]
State after:
no goals