showPs env ((n, _, Let _ t v):bs)
    = "  " ++ show n ++ " : " ++
      showEnv env ({- normalise ctxt env -} t) ++ "   =   " ++
      showEnv env ({- normalise ctxt env -} v) ++
      "\n" ++ showPs env bs
showPs env ((n, _, b):bs)
    = "  " ++ show n ++ " : " ++
      showEnv env ({- normalise ctxt env -} (binderTy b)) ++
      "\n" ++ showPs env bs