diff --git a/trans/statics.stx b/trans/statics.stx
index b6a7d83..ef63c8d 100644
--- a/trans/statics.stx
+++ b/trans/statics.stx
@@ -139,11 +139,16 @@ hand-defined, as done in "statics/util.stx" like so:
     type_OptTermEx(ote) == T,
     @l.type := T.
 
-  type_Ex : Ex -> TYPE
+  type_Ex     :     Ex -> TYPE
+  type_TermEx : TermEx -> TYPE
 
   type_OptTermEx(ote@Ex2OptTermEx(e)) = T :-
     type_Ex(e) == T,
-    @ote.type :=T.
+    @ote.type := T.
+
+  type_OptTermEx(ote@TermEx2OptTermEx(te)) = T :-
+    type_TermEx(te) == T,
+    @ote.type := T.
 
   /** md
 
@@ -171,8 +176,6 @@ constructor was trivial:
 ```
   **/
 
-  type_TermEx: TermEx -> TYPE
-
   type_TermEx(te@Terminate(e)) = T :-
     type_Ex(e) == T,
     @te.type := T.