- TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
- | prod: ∀G.∀A,B.∀i,j,k. R i j k →
- TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
+ TJ p G A B → TJ p G C (Sort i) →
+ TJ p (C::G) (lift A 0 1) (lift B 0 1)
+ | prod: ∀G.∀A,B.∀i,j,k. Re p i j k →
+ TJ p G A (Sort i) → TJ p (A::G) B (Sort j) →
+ TJ p G (Prod A B) (Sort k)