X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Fvpushs_fold.ma;h=8ac1699861e2c7751fcc34c38fd31e26d7bd645f;hp=59f9b3e84fa4a49b717fcf69c9693e0f09650c1f;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma
index 59f9b3e84..8ac169986 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma
@@ -21,8 +21,8 @@ include "apps_2/models/vpushs.ma".
 
 lemma vpushs_fold (M): is_model M → is_extensional M →
                        ∀L,T1,T2,gv,lv.
-                       (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]) → 
-                       ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv].
+                       (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv,v] ≗ ⟦T2⟧[gv,v]) → 
+                       ⟦L+T1⟧[gv,lv] ≗{M} ⟦L+T2⟧[gv,lv].
 #M #H1M #H2M #L elim L -L [| #K * [| * ]]
 [ #T1 #T2 #gv #lv #H12
   >fold_atom >fold_atom
@@ -44,8 +44,8 @@ qed.
 (* Inversion lemmas with fold for restricted closures ***********************)
 
 lemma vpushs_inv_fold (M): is_model M → is_injective M →
-                           ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv] →
-                           ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v].
+                           ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv,lv] ≗{M} ⟦L+T2⟧[gv,lv] →
+                           ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv,v] ≗ ⟦T2⟧[gv,v].
 #M #H1M #H2M #L elim L -L [| #K * [| * ]]
 [ #T1 #T2 #gv #lv
   >fold_atom >fold_atom #H12 #v #H