[Reduced the universe level of a type.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080305025947] hunk ./Wand.agda 307
-  data Exp' : (t : Ty) -> ⟦ t ⟧⋆ -> Set1 where
+  data Exp' : (t : Ty) -> ⟦ t ⟧⋆ -> Set where