(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/Inc/defs".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Inc/defs".
(* DISPLACEMENT INCREMENT RELATION
*)
-include "logic/equality.ma".
-
-include "P/defs.ma".
+include "SUB/Term/defs.ma".
inductive Inc (i:Nat): Bool \to Head \to Nat \to Prop \def
- | inc_bind: \forall x. Inc i true (bind x) (succ i)
- | inc_flat: \forall y. Inc i true (flat y) i
- | inc_neg : \forall z. Inc i false z i
+ | inc_bind: \forall r. Inc i true (bind r) (succ i)
+ | inc_skip: \forall r. Inc i false (bind r) i
+ | inc_flat: \forall r,q. Inc i q (flat r) i
.