λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / frees_fqup.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
index feb74eb263f4fc3d49639e1d98d91c8c9b114005..68544e7b0a0fea49bcb6df417a81f79a916786b3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
@@ -109,7 +109,7 @@ lemma frees_ind_void (Q:relation3 …):
         ∀f,i. 𝐈⦃f⦄ →  Q (⋆) (#i) (⫯*[i]↑f)
       ) → (
         ∀f,I,L,V.
-        L ⊢ 𝐅+⦃V⦄ ≘ f →  Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f) 
+        L ⊢ 𝐅+⦃V⦄ ≘ f →  Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f)
       ) → (
         ∀f,I,L. 𝐈⦃f⦄ →  Q (L.ⓤ{I}) (#O) (↑f)
       ) → (