\ /
V_______________________________________________________________ *)
-include "lambda/reduction.ma".
-
+include "pts_dummy/reduction.ma".
+(*
(*
inductive T : Type[0] ≝
| Sort: nat → T
|@(ex_intro … M) @(ex_intro … M) % // % //
]
*)
+*)
\ No newline at end of file