mutual
  U :: Set
    = data Nhat | Finzerohat | Finonehat | Boolhat | Sigmahat (a :: U) (b:: T a -> U) 
           | Pihat (a:: U) (b:: T a -> U)
  
  T (a :: U)
    :: Set
    = {! !}