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