\ /
V_______________________________________________________________ *)
-include "lambda/types.ma".
-
+include "pts_dummy/types.ma".
+(*
(*
inductive TJ (p: pts): list T → T → T → Prop ≝
| ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j)
]
qed.
+*)