diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index c4bcac4..de4d7bb 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -318,17 +318,20 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
 
   namespace Term
     export covering %inline
-    equal, sub : (ty, s, t : Term q d n) -> m ()
+    equal, sub, super : (ty, s, t : Term q d n) -> m ()
     equal = compare Equal
     sub   = compare Sub
+    super = compare Super
 
     export covering %inline
-    equalType, subtype : (s, t : Term q d n) -> m ()
+    equalType, subtype, supertype : (s, t : Term q d n) -> m ()
     equalType = compareType Equal
     subtype   = compareType Sub
+    supertype = compareType Super
 
   namespace Elim
     export covering %inline
-    equal, sub : (e, f : Elim q d n) -> m ()
+    equal, sub, super : (e, f : Elim q d n) -> m ()
     equal = compare Equal
     sub   = compare Sub
+    super = compare Super