(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/A/defs".
-
-include "preamble.ma".
+include "LambdaDelta-1/preamble.ma".
inductive A: Set \def
| ASort: nat \to (nat \to A)