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=37bd15ada9016789cd7ce90baff4b2e18bd8030a;hp=4eafa94d2205b9db2452f19901f724ce5c592f0e;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

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 4eafa94d2..37bd15ada 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
@@ -20,7 +20,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 →
-                       ⦃G, L, U⦄ ⊐+[b] ⦃G, K, T⦄.
+                       ⦃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
   #I #Y #HY #H destruct <(drops_fwd_isid … HY) -K //
@@ -33,7 +33,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 →
-                         ⦃G1, K1, T1⦄ ⊐[b] ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, K2, T2⦄.
+                         ⦃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
   >(drops_fwd_isid … HLK1) -L1 //
@@ -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.