{-# LANGUAGE UnicodeSyntax #-}

lengthOP n (⊜) = 0 ⊜ n