diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt
index a54338d..86a6e2e 100644
--- a/cur-lib/cur/curnel/redex-core.rkt
+++ b/cur-lib/cur/curnel/redex-core.rkt
@@ -445,14 +445,15 @@
    ,(and (term (nonpositive x t_0)) (term (positive x t)))]
   [(positive x t) #t])
 
-(define-metafunction tt-typingL
-  positive* : x (t ...) -> #t or #f
-  [(positive* D ()) #t]
-  [(positive* D (t_c t_rest ...))
-   ;; Replace the result of the constructor with (Unv 0), to avoid the result being considered a
-   ;; nonpositive position.
-   ,(and (term (positive D (in-hole Ξ (Unv 0)))) (term (positive* D (t_rest ...))))
-   (where (in-hole Ξ (in-hole Θ D)) t_c)])
+;; Holds when the type t is a valid type for a constructor of D
+(define-judgment-form tt-typingL
+  #:mode (valid-constructor I I)
+  #:contract (valid-constructor D t)
+
+  ;; NB TODO: Ignore the "positive" occurrence of D in the result; this is hacky way to do this
+  [(side-condition (positive D (in-hole Ξ (Unv 0))))
+   ---------------------------------------------------------
+   (valid-constructor D (name t_c (in-hole Ξ (in-hole Θ D))))])
 
 ;; Holds when the signature Δ is valid
 (define-judgment-form tt-typingL
@@ -464,15 +465,10 @@
 
   [(valid Δ)
    (type-infer Δ ∅ t_D U_D)
+   (valid-constructor D t_c) ...
    (type-infer Δ (∅ D : t_D) t_c U_c) ...
-   ;; NB: Ugh this should be possible with pattern matching alone ....
-   (side-condition ,(andmap (curry equal? (term D)) (term (D_0 ...))))
-   (side-condition (positive* D (t_c ...)))
    ----------------- "Valid-Inductive"
-   (valid (Δ (D : t_D
-               ;; Checks that a constructor for x actually produces an x, i.e., that
-               ;; the constructor is well-formed.
-               ((c : (name t_c (in-hole Ξ (in-hole Θ D_0)))) ...))))])
+   (valid (Δ (D : t_D ((c : t_c) ...))))])
 
 ;; Holds when the signature Δ and typing context Γ are well-formed.
 (define-judgment-form tt-typingL
diff --git a/cur-test/cur/tests/redex-core.rkt b/cur-test/cur/tests/redex-core.rkt
index c47af7d..30c6556 100644
--- a/cur-test/cur/tests/redex-core.rkt
+++ b/cur-test/cur/tests/redex-core.rkt
@@ -225,19 +225,26 @@
 ;; Test static semantics
 ;; ------------------------------------------------------------------------
 
-(check-true (term (positive* nat (nat))))
-(check-true (term (positive* nat ((Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))))
-(check-true (term (positive* nat ((Π (x : nat) nat)))))
+(check-holds
+ (valid-constructor nat nat))
+(check-holds
+ (valid-constructor nat (Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))
+(check-holds
+ (valid-constructor nat (Π (x : nat) nat)))
 ;; (nat -> nat) -> nat
 ;; Not sure if this is actually supposed to pass
-(check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
+(check-not-holds
+ (valid-constructor nat (Π (x : (Π (y : nat) nat)) nat)))
 ;; ((Unv 0) -> nat) -> nat
-(check-true (term (positive* nat ((Π (x : (Π (y : (Unv 0)) nat)) nat)))))
+(check-holds
+ (valid-constructor nat (Π (x : (Π (y : (Unv 0)) nat)) nat)))
 ;; (((nat -> (Unv 0)) -> nat) -> nat)
-(check-true (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))))
+(check-holds
+ (valid-constructor nat (Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))
 ;; Not sure if this is actually supposed to pass
 ;; ((nat -> nat) -> nat) -> nat
-(check-false (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))))
+(check-not-holds
+ (valid-constructor nat (Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))
 
 (check-true (judgment-holds (wf ,Δ0 ∅)))
 (check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
@@ -280,7 +287,8 @@
 (check-holds (type-infer ∅ ∅ (Unv 0) U))
 (check-holds (type-infer ∅ (∅ nat : (Unv 0)) nat U))
 (check-holds (type-infer ∅ (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
-(check-true (term (positive* nat (nat (Π (x : nat) nat)))))
+(check-holds (valid-constructor nat nat))
+(check-holds (valid-constructor nat (Π (x : nat) nat)))
 (check-holds
  (wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
 (check-holds