pub fn nec_not_lob( ) -> Nec<Not<Imply<Nec<Imply<Nec<False>, False>>, Nec<False>>>>
□¬(□(□⊥ => ⊥) => □⊥).
□¬(□(□⊥ => ⊥) => □⊥)