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.ma;h=ed7315b8cd4663db0168a5c766ad3fc98ad47299;hp=91a2ab2a914818c4ed9e18f22056e0fe9f3b651f;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

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 91a2ab2a9..ed7315b8c 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 *)