pub fn para_lob(x: Imply<Nec<Imply<Nec<False>, False>>, Nec<False>>) -> False
⊥^(□(□⊥ => ⊥) => □⊥).
⊥^(□(□⊥ => ⊥) => □⊥)