diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index a9bdbd9..4ec000a 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -74,7 +74,11 @@ data IsSubj : Qty -> Type where
   SZero : IsSubj Zero
   SOne  : IsSubj One
 
+export Uninhabited (IsSubj Any) where uninhabited _ impossible
+
 public export
 data IsGlobal : Qty -> Type where
   GZero : IsGlobal Zero
   GAny  : IsGlobal Any
+
+export Uninhabited (IsGlobal One) where uninhabited _ impossible