case base.succ
n✝ : ℕ
⊢ ¬0 = n✝ + 1
x : Tree Unit
n : ℕ
⊢ x ∈ treesOfNumNodesEq n ↔ numNodes x = n
induction x using Tree.unitRecOn generalizing n <;> cases n <;>
  simp [treesOfNumNodesEq_succ, Nat.succ_eq_add_one, *]
no goals
case base.succ
n✝ : ℕ
⊢ ¬0 = n✝ + 1
exact (Nat.succ_ne_zero _).symm