ground_2 released and permanently renamed as ground

[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..00b3e4fed9950602335f9fd9ee5f6a5d90f570dd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/lib/star.ma".
+include "ground/lib/star.ma".
 include "static_2/notation/relations/suptermplus_6.ma".
 include "static_2/notation/relations/suptermplus_7.ma".
 include "static_2/s_transition/fqu.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 *)