simp_arith
case node_case.cons
x : Nat
head✝ : NatTree
tail✝ : List NatTree
ih :
  (∀ (t2 : NatTree), size (splice head✝ t2) = size head✝ + size t2) ∧
    all (fun t1 => ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2) tail✝
⊢ ∀ (t2 : NatTree), 1 + (size head✝ + size t2 + nodeListSize tail✝) = 1 + (size head✝ + nodeListSize tail✝) + size t2
no goals