X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FUnified%2FSUB%2FLift%2Fdefs.ma;h=0806d35e62b97ec08dbd2d78296e56b2fe94c3dc;hb=52c5033a45003a9488f0687510554b5efb4dd84e;hp=a6c3345caa4be6dd7e7863a4e66999eec3345a50;hpb=803d665cbff289f5e5340b9db137f1c4685b43f9;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
index a6c3345ca..0806d35e6 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
@@ -12,30 +12,28 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/Lift/defs".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
 
 (* LIFT RELATION
    - Usage: invoke with positive polarity
 *)
 
-include "logic/equality.ma".
-include "../../RELATIONAL/NPlus/defs.ma".
-include "../../RELATIONAL/NLE/defs.ma".
-include "../../RELATIONAL/BEq/defs.ma".
+include "SUB/Switch/defs.ma".
+include "SUB/Inc/defs.ma".
 
-include "P/defs.ma".
-include "Inc/defs.ma".
-
-inductive Lift (l: Nat): Nat \to Bool \to P \to P \to Prop \def
-   | lift_sort    : \forall i,a,h. Lift l i a (sort h) (sort h)
-   | lift_lref_neg: \forall i,j. Lift l i false (lref j) (lref j)
-   | lift_lref_lt : \forall i,j. 
-                    j < i \to Lift l i true (lref j) (lref j)
-   | lift_lref_ge : \forall i,j1,j2.
-                    i <= j1 \to (j1 + l == j2) \to
-                    Lift l i true (lref j1) (lref j2)
-   | lift_head    : \forall i,i',a,b,a',z,q1,q2,p1,p2. 
-                    (a * b == a') \to Inc i a' z i' \to
-                    Lift l i a' q1 q2 \to Lift l i' a p1 p2 \to 
-                    Lift l i a (head b z q1 p1) (head b z q2 p2)
+inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
+   | lift_sort   : \forall l,q,i,h. 
+                   Lift q l i (leaf (sort h)) (leaf (sort h))
+   | lift_skip   : \forall l,i,j. 
+                   Lift false l i (leaf (lref j)) (leaf (lref j))
+   | lift_lref_lt: \forall l,i,j. j < i \to 
+                   Lift true l i (leaf (lref j)) (leaf (lref j))
+   | lift_lref_ge: \forall l,i,j1. i <= j1 \to
+                   \forall j2. (j1 + l == j2) \to
+                   Lift true l i (leaf (lref j1)) (leaf (lref j2))
+   | lift_head   : \forall l,qt,qu,z. Switch qt z qu \to
+                   \forall iu,it. Inc qt iu z it \to
+                   \forall u1,u2. Lift qu l iu u1 u2 \to
+                   \forall t1,t2. Lift qt l it t1 t2 \to 
+                   Lift qt l iu (head z u1 t1) (head z u2 t2)
 .