X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_computation%2Ffqup_drops.ma;h=2b5173d75bfbb82709e3a043b1a5ad92347252e9;hp=2a81feacffc91d16f27083e8661d094f3e8dad31;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma
index 2a81feacf..2b5173d75 100644
--- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma
@@ -19,7 +19,7 @@ include "static_2/s_computation/fqup.ma".
 
 (* Properties with generic slicing for local environments *******************)
 
-lemma fqup_drops_succ: ∀b,G,K,T,i,L,U. ⇩*[↑i] L ≘ K → ⇧*[↑i] T ≘ U →
+lemma fqup_drops_succ: ∀b,G,K,T,i,L,U. ⇩[↑i] L ≘ K → ⇧[↑i] T ≘ U →
                        ❪G,L,U❫ ⬂+[b] ❪G,K,T❫.
 #b #G #K #T #i elim i -i
 [ #L #U #HLK #HTU elim (drops_inv_succ … HLK) -HLK
@@ -32,7 +32,7 @@ lemma fqup_drops_succ: ∀b,G,K,T,i,L,U. ⇩*[↑i] L ≘ K → ⇧*[↑i] T ≘
 ]
 qed.
 
-lemma fqup_drops_strap1: ∀b,G1,G2,L1,K1,K2,T1,T2,U1,i. ⇩*[i] L1 ≘ K1 → ⇧*[i] T1 ≘ U1 →
+lemma fqup_drops_strap1: ∀b,G1,G2,L1,K1,K2,T1,T2,U1,i. ⇩[i] L1 ≘ K1 → ⇧[i] T1 ≘ U1 →
                          ❪G1,K1,T1❫ ⬂[b] ❪G2,K2,T2❫ → ❪G1,L1,U1❫ ⬂+[b] ❪G2,K2,T2❫.
 #b #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 *
 [ #HLK1 #HTU1 #HT12
@@ -42,5 +42,5 @@ lemma fqup_drops_strap1: ∀b,G1,G2,L1,K1,K2,T1,T2,U1,i. ⇩*[i] L1 ≘ K1 → 
 ]
 qed-.
 
-lemma fqup_lref: ∀b,I,G,L,K,V,i. ⇩*[i] L ≘ K.ⓑ[I]V → ❪G,L,#i❫ ⬂+[b] ❪G,K,V❫.
+lemma fqup_lref: ∀b,I,G,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L,#i❫ ⬂+[b] ❪G,K,V❫.
 /2 width=6 by fqup_drops_strap1/ qed.