diff --git a/tests/TermImpls.idr b/tests/TermImpls.idr
new file mode 100644
index 0000000..b14aaac
--- /dev/null
+++ b/tests/TermImpls.idr
@@ -0,0 +1,90 @@
+module TermImpls
+
+import Quox.Syntax
+import Quox.Pretty
+
+
+private
+eqShift : Shift from1 to -> Shift from2 to -> Maybe (from1 = from2)
+eqShift SZ      SZ      = Just Refl
+eqShift (SS by) (SS bz) = eqShift by bz
+eqShift SZ      (SS by) = Nothing
+eqShift (SS by) SZ      = Nothing
+
+private
+eqSubst : Subst tm1 from1 to -> Subst tm2 from2 to -> Maybe (from1 = from2)
+eqSubst (Shift by) (Shift bz) = eqShift by bz
+eqSubst (_ ::: th) (_ ::: ph) = cong S <$> eqSubst th ph
+eqSubst (Shift _)  (_ ::: _)  = Nothing
+eqSubst (_ ::: _)  (Shift _)  = Nothing
+  -- maybe from1 = from2 in the last two cases, but this is for
+  -- (==), and they're not equal, so who cares
+
+mutual
+  export covering
+  Eq (Term d n) where
+    TYPE k == TYPE l = k == l
+    TYPE _ == _ = False
+
+    Pi qty1 _ arg1 res1 == Pi qty2 _ arg2 res2 =
+      qty1 == qty2 && arg1 == arg2 && res1 == res2
+    Pi {} == _ = False
+
+    Lam _ body1 == Lam _ body2 = body1 == body2
+    Lam {} == _ = False
+
+    E e == E f = e == f
+    E _ == _ = False
+
+    CloT tm1 th1 == CloT tm2 th2 =
+      case eqSubst th1 th2 of
+           Just Refl => tm1 == tm2 && th1 == th2
+           Nothing   => False
+    CloT {} == _ = False
+
+    DCloT tm1 th1 == DCloT tm2 th2 =
+      case eqSubst th1 th2 of
+           Just Refl => tm1 == tm2 && th1 == th2
+           Nothing   => False
+    DCloT {} == _ = False
+
+  export covering
+  Eq (Elim d n) where
+    F x == F y = x == y
+    F _ == _ = False
+
+    B i == B j = i == j
+    B _ == _ = False
+
+    (fun1 :@ arg1) == (fun2 :@ arg2) = fun1 == fun2 && arg1 == arg2
+    (_ :@ _) == _ = False
+
+    (tm1 :# ty1) == (tm2 :# ty2) = tm1 == tm2 && ty1 == ty2
+    (_ :# _) == _ = False
+
+    CloE el1 th1 == CloE el2 th2 =
+      case eqSubst th1 th2 of
+           Just Refl => el1 == el2 && th1 == th2
+           Nothing   => False
+    CloE {} == _ = False
+
+    DCloE el1 th1 == DCloE el2 th2 =
+      case eqSubst th1 th2 of
+           Just Refl => el1 == el2 && th1 == th2
+           Nothing   => False
+    DCloE {} == _ = False
+
+  export covering
+  Eq (ScopeTerm d n) where
+    TUsed   s == TUsed   t = s == t
+    TUnused s == TUnused t = s == t
+    TUsed   _ == TUnused _ = False
+    TUnused _ == TUsed   _ = False
+
+export covering
+Show (Term d n) where
+  showPrec d t = showParens (d /= Open) $ prettyStr True t
+
+export covering
+Show (Elim d n) where
+  showPrec d e = showParens (d /= Open) $ prettyStr True e