zify
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ ↑(lengthOf X) < ↑(lengthOf Y) ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)