X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fapps_2%2Ffunctional%2Fsubst.ma;h=e8ba1c2f25e29fef1f3a509d78d7449415f7129a;hb=913512bbc9202f2109d53acd43dc8c0270b17184;hp=6aa75625d26e063e5d27fd4a2971639a685f464e;hpb=eb918fc784eacd2094e3986ba321ef47690d9983;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
index 6aa75625d..e8ba1c2f2 100644
--- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/unfold/delift_lift.ma".
-include "Apps_2/functional/lift.ma".
+include "basic_2/unfold/delift_lift.ma".
+include "apps_2/functional/lift.ma".
 
 (* CORE SUBSTITUTION ********************************************************)
 
@@ -52,21 +52,21 @@ theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
                            L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
 #K #V #T1 elim T1 -T1
 [ * #i #L #T2 #d #HLK #H
-  [ -HLK >(delift_fwd_sort1 … H) -H //
+  [ -HLK >(delift_inv_sort1 … H) -H //
   | elim (lt_or_eq_or_gt i d) #Hid normalize
-    [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/
+    [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/
     | destruct
-      elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
+      elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
       lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
       >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
-    | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/
+    | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/
     ]
-  | -HLK >(delift_fwd_gref1 … H) -H //
+  | -HLK >(delift_inv_gref1 … H) -H //
   ]
 | * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
-  [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
     <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
-  | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
     <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
   ]
 ]