diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr
index c7d5e02..1945936 100644
--- a/lib/Quox/Displace.idr
+++ b/lib/Quox/Displace.idr
@@ -2,6 +2,8 @@ module Quox.Displace
 
 import Quox.Syntax
 
+%default total
+
 
 parameters (k : Universe)
   namespace Term
@@ -31,7 +33,7 @@ parameters (k : Universe)
     doDisplace (Box val loc) = Box (doDisplace val) loc
     doDisplace (E e) = E (doDisplace e)
     doDisplace (CloT (Sub t th)) =
-      CloT (Sub (doDisplace t) (map doDisplace th))
+      CloT (Sub (doDisplace t) (assert_total $ map doDisplace th))
     doDisplace (DCloT (Sub t th)) =
       DCloT (Sub (doDisplace t) th)
 
@@ -48,7 +50,8 @@ parameters (k : Universe)
     doDisplace (CasePair qty pair ret body loc) =
       CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
     doDisplace (CaseEnum qty tag ret arms loc) =
-      CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc
+      CaseEnum qty (doDisplace tag) (doDisplaceS ret)
+               (assert_total $ map doDisplace arms) loc
     doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =
       CaseNat qty qtyIH (doDisplace nat) (doDisplaceS ret)
               (doDisplace zero) (doDisplaceS succ) loc
@@ -65,9 +68,9 @@ parameters (k : Universe)
            (doDisplaceDS zero) (doDisplaceDS one) loc
     doDisplace (TypeCase ty ret arms def loc) =
       TypeCase (doDisplace ty) (doDisplace ret)
-               (map doDisplaceS arms) (doDisplace def) loc
+               (assert_total $ map doDisplaceS arms) (doDisplace def) loc
     doDisplace (CloE (Sub e th)) =
-      CloE (Sub (doDisplace e) (map doDisplace th))
+      CloE (Sub (doDisplace e) (assert_total $ map doDisplace th))
     doDisplace (DCloE (Sub e th)) =
       DCloE (Sub (doDisplace e) th)