VOID : Ty n
VOID = Mu $ TVar FZ

exfalso : Term {n=0} g (VOID ~> a)
exfalso = Cata $ Lam $ Var Here

data Term : List (Ty n) -> Ty n -> Type where
  TT   : Term g U
  Var  : Elem a g -> Term g a
  Lam  : Term (a::g) b -> Term g (a~>b)
  App  : {a : Ty 0} -> Term g (a~>b) -> Term g a -> Term g b
  Pair : Term g a -> Term g b -> Term g (Prod a b)
  Fst  : Term g (Prod a b) -> Term g a
  Snd  : Term g (Prod a b) -> Term g b
  Inl  : Term g a -> Term g (Sum a b)
  Inr  : Term g b -> Term g (Sum a b)
  Case : {a, b : Ty n} -> Term g (Sum a b) -> Term (a::g) c -> Term (b::g) c -> Term g c
  In   : Term g (subst1T f (Mu f)) -> Term g (Mu f)
  Cata : Term g (subst1T f a ~> a) -> Term g (Mu f ~> a)