update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / s_computation / fqup.ma

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 91a2ab2a914818c4ed9e18f22056e0fe9f3b651f..ed7315b8cd4663db0168a5c766ad3fc98ad47299 100644 (file)
--- 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 *)