X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_computation%2Ffqup.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_computation%2Ffqup.ma;h=1f21d404ef32fbdc70ff20e02bf3863e8d009a06;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=28cfb9ce0c5c928cfea1bb6f6b06a67af7c038c8;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
index 28cfb9ce0..1f21d404e 100644
--- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
@@ -86,7 +86,7 @@ qed-.
 (* Advanced properties ******************************************************)
 
 lemma fqup_zeta (b) (p) (I) (G) (K) (V):
-                ∀T1,T2. ⬆*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⬂+[b] ⦃G,K,T2⦄.
+                ∀T1,T2. ⇧*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⬂+[b] ⦃G,K,T2⦄.
 * /4 width=5 by fqup_strap2, fqu_fqup, fqu_drop, fqu_clear, fqu_bind_dx/ qed.
 
 (* Basic_2A1: removed theorems 1: fqup_drop *)