unified: some theorems on Lift started

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Unified-Sub / Lift / defs.ma

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 cf29a3562e573ceda4071a0acdaaa88bc62ee32c..eac00ae357c40fcba2723dd85f1b7e3067c7c325 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
@@ -18,21 +18,29 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
    - Usage: invoke with positive polarity
 *)
 
-include "Inc/defs.ma".
+include "Term/defs.ma".
 
 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_lref   : \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,q. (qt -- q == qu) \to
-                   \forall z,iu,it. Inc iu qu 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 q z u1 t1) (head q z u2 t2)
+   | lift_bind   : \forall l,i,u1,u2. Lift true l i u1 u2 \to
+                   \forall q,t1,t2. Lift q l (succ i) t1 t2 \to 
+                   \forall r.
+                   Lift q l i (head q (bind r) u1 t1) (head q (bind r) u2 t2)
+   | lift_flat   : \forall l,i,u1,u2. Lift true l i u1 u2 \to
+                   \forall q,t1,t2. Lift q l i t1 t2 \to 
+                   \forall r.
+                   Lift q l i (head q (flat r) u1 t1) (head q (flat r) u2 t2)
+   | lift_head   : \forall l,q,p. (p = q \to False) \to
+                   \forall i,u1,u2. Lift false l i u1 u2 \to
+                   \forall t1,t2. Lift q l i t1 t2 \to 
+                   \forall z.
+                   Lift q l i (head p z u1 t1) (head p z u2 t2)
 .