(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
-
-include "Lift/fun.ma".
+include "Unified-Sub/Lift/fun.ma".
(* NOTE: this holds because of nplus_comm_1 *)
theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to