have : ∀ W, zlengthOfSet W = lengthOfSet W := by intro W; simp
X Y : Finset Formula
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y