(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
-
(* LIFT RELATION
- Usage: invoke with positive polarity
*)
-include "datatypes/Term.ma".
+include "Unified-Sub/datatypes/Term.ma".
inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
| lift_sort : \forall i,h.