-data OList : [low upp : Lift] -> * =>
- { onil : le' low upp -> OList low upp
- | ocons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp
+data OList : [low upp : Lift] → ⋆ ⇒
+ { onil : le' low upp → OList low upp
+ | ocons : [n : Nat] → OList (lift n) upp → le' low (lift n) → OList low upp