-axiom conv: T → T → Prop.
-
-inductive TJ: list T → T → T → Prop ≝
- | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
- | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
+axiom conv: T → T → Prop.*)
+
+inductive TJ
+ (S: nat → nat → Prop)
+ (R: nat → nat → nat → Prop)
+ (c: T → T → Prop) : list T → T → T → Prop ≝
+ | ax : ∀i,j. S i j → TJ S R c (nil T) (Sort i) (Sort j)
+ | start: ∀G.∀A.∀i.TJ S R c G A (Sort i) →
+ TJ S R c (A::G) (Rel 0) (lift A 0 1)