data Pref : a -> List a -> a -> List a -> Type where
  ShiftP : Pref x xs y (x::xs)
  ThereP : Pref x xs y ys -> Pref x xs z (y::ys)

comp : Term ph g (Box [a] b ~> Box [a] (Box [b] c) ~> Box [a] c)
comp = Lam $ Lam $
       Shut $ Open HereP
             (Open ShiftP (Var Here)) -- {e=[Var Here]}
             {e=[Open ShiftP (Var $ There Here)]} --{e=[Var Here]}

comp : Term d g (Box [a] b ~> Box [a] (Box [b] c) ~> Box [a] c)
comp = Lam $ Lam $ Letbox (Var $ There Here) $
                   Letbox (Var Here) $
                   Shut $
                   Letbox (MVar Here) -- {e=[Var Here]}
                          (MVar Here) -- {e=[MVar (There $ There Here) {e=[Var Here]}]}