\ /
V_______________________________________________________________ *)
-include "lambda/reduction.ma".
-include "lambda/inversion.ma".
-
+include "pts_dummy/reduction.ma".
+include "pts_dummy/inversion.ma".
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
]
qed.
+*)