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

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
index dabd2c431..34e9de237 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
@@ -20,7 +20,7 @@ include "apps_2/models/veq.ma".
 
 inductive vpushs (M) (gv) (lv): relation2 lenv (evaluation M) ≝
 | vpushs_atom: vpushs M gv lv (⋆) lv
-| vpushs_abbr: ∀v,d,K,V. vpushs M gv lv K v → ⟦V⟧[gv, v] = d → vpushs M gv lv (K.ⓓV) (⫯[0←d]v)
+| vpushs_abbr: ∀v,d,K,V. vpushs M gv lv K v → ⟦V⟧[gv,v] = d → vpushs M gv lv (K.ⓓV) (⫯[0←d]v)
 | vpushs_abst: ∀v,d,K,V. vpushs M gv lv K v → vpushs M gv lv (K.ⓛV) (⫯[0←d]v)
 | vpushs_unit: ∀v,d,I,K. vpushs M gv lv K v → vpushs M gv lv (K.ⓤ{I}) (⫯[0←d]v)
 | vpushs_repl: ∀v1,v2,L. vpushs M gv lv L v1 → v1 ≗ v2 → vpushs M gv lv L v2
@@ -51,7 +51,7 @@ lemma vpushs_inv_atom (M) (gv) (lv): is_model M →
 fact vpushs_inv_abbr_aux (M) (gv) (lv): is_model M →
                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
                                         ∀K,V. K.ⓓV = L →
-                                        ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv, v]]v ≗ y.
+                                        ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv,v]]v ≗ y.
 #M #gv #lv #HM #y #L #H elim H -y -L
 [ #Y #X #H destruct
 | #v #d #K #V #Hv #Hd #_ #Y #X #H destruct
@@ -66,7 +66,7 @@ qed-.
 
 lemma vpushs_inv_abbr (M) (gv) (lv): is_model M →
                                      ∀y,K,V. K.ⓓV ⨁{M}[gv] lv ≘ y →
-                                     ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv, v]]v ≗ y.
+                                     ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv,v]]v ≗ y.
 /2 width=3 by vpushs_inv_abbr_aux/ qed-.
 
 fact vpushs_inv_abst_aux (M) (gv) (lv): is_model M →