Thanks to Guarrigue, code for Serializer functor simplified using

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / delift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
index 7620ae092723b24509615d28f3bc46c14617760c..f0935a0413c9b36d6e8b82d4863ca48ab913f7c1 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
@@ -14,21 +14,25 @@
 
 include "basic_2/unfold/tpss.ma".
 
-(* DELIFT ON TERMS **********************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
 definition delift: nat → nat → lenv → relation term ≝
-                   λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ▶* T & ⇧[d, e] T2 ≡ T.
+                   λd,e,L,T1,T2. ∃∃T. L ⊢ T1 ▶* [d, e] T & ⇧[d, e] T2 ≡ T.
 
-interpretation "delift (term)"
+interpretation "inverse basic relocation (term)"
    'TSubst L T1 d e T2 = (delift d e L T1 T2).
 
 (* Basic properties *********************************************************)
 
+lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 →
+                   ∀L. L ⊢ T2 [d, e] ≡ T1.
+/2 width=3/ qed.
+
 lemma delift_refl_O2: ∀L,T,d. L ⊢ T [d, 0] ≡ T.
 /2 width=3/ qed.
 
 lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 →
-                         ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡ T2.
+                         ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡ T2.
 #L1 #T1 #T2 #d #e * /3 width=3/
 qed.