(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term".
+
(* POLARIZED TERMS
- Naming policy:
- terms : t u
*)
-include "preamble.ma".
+include "preamble4.ma".
inductive Bind: Type \def
| abbr: Bind