Theorem: List.length_ofFn (LeanSAT/Reflect/BoolExpr/Nat.lean)

State before:
k : Nat
α : Type u_1
f : Fin k → α
⊢ (ofFn f).length = k
Tactic:
simp [ofFn, length_ofFn_go]
State after:
no goals