\ /
V_______________________________________________________________ *)
-include "lambda/par_reduction.ma".
+include "pts_dummy/par_reduction.ma".
include "basics/star.ma".
-
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
@red_subst1 //
]
qed.
-
-
-
-
+*)