apply Finset.sum_induction zlengthOf
X : Finset Formula
⊢ zlengthOfSet X ≥ 0
case hom
X : Finset Formula
⊢ ∀ (a b : ℤ), 0 ≤ a → 0 ≤ b → 0 ≤ a + b

case unit
X : Finset Formula
⊢ 0 ≤ 0

case base
X : Finset Formula
⊢ ∀ x ∈ X, 0 ≤ zlengthOf x