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

State before:
x : Nat
t : NatTree
ts : List NatTree
t2 : NatTree
⊢ splice (node x (t :: ts)) t2 = node x (splice t t2 :: ts)
Tactic:
rw[splice]
State after:
no goals