Theorem: Cpdt.Chapter3.NatTree.nodeListSize_cons (Cpdt/Chapter3/Nested.lean)

State before:
t : NatTree
ts : List NatTree
⊢ nodeListSize (t :: ts) = size t + nodeListSize ts
Tactic:
rw[nodeListSize]
State after:
no goals