X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Ffunctional%2Fsubst.ma;h=05f698ff8fb9931a7b5357efae2252d7b4541710;hb=0aa60d67f17b528b896e05bbd01038cbc195f69d;hp=5c92a129312e272085f34d31a2f20e8dcd4841e9;hpb=62a926c1a14562bf158941156c6032c0c8d86fbe;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
index 5c92a1293..05f698ff8 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
@@ -20,7 +20,7 @@ include "Basic_2/functional/lift.ma".
 let rec fsubst W d U on U ≝ match U with
 [ TAtom I     ⇒ match I with
   [ Sort _ ⇒ U
-  | LRef i ⇒ tri … i d (#i) (↟[0, i] W) (#(i-1))
+  | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1))
   | GRef _ ⇒ U
   ]
 | TPair I V T ⇒ match I with
@@ -34,7 +34,7 @@ interpretation "functional core substitution" 'Subst V d T = (fsubst V d T).
 (* Main properties **********************************************************)
 
 theorem fsubst_delift: ∀K,V,T,L,d.
-                       ↓[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ ↡[d ← V] T.
+                       ⇓[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ ↓[d ← V] T.
 #K #V #T elim T -T
 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
   elim (lt_or_eq_or_gt i d) #Hid
@@ -48,8 +48,8 @@ qed.
 
 (* Main inversion properties ************************************************)
 
-theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ↓[0, d] L ≡ K. 𝕓{Abbr} V →
-                           L ⊢ T1 [d, 1] ≡ T2 → ↡[d ← V] T1 = T2.
+theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇓[0, d] L ≡ K. 𝕓{Abbr} 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 //
@@ -71,4 +71,3 @@ theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ↓[0, d] L ≡ K. 𝕓{Abbr} V →
   ]
 ]
 qed-.
- 
\ No newline at end of file