- lazy extended reduction parked

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fpbc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma
index 4656f843190567ebf4584f96fb37329f758d847c..bf9baaa90c50ddd87d86f801a0eeb3278807fb87 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma
@@ -20,7 +20,7 @@ include "basic_2/computation/fpbu.ma".
 
 definition fpbc: ∀h. sd h → tri_relation genv lenv term ≝
                  λh,g,G1,L1,T1,G2,L2,T2.
-                 ∃∃G,L,T.  ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄ .
+                 ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄.
 
 interpretation
    "single-step 'big tree' proper parallel reduction (closure)"