update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / models / vpushs.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
index dabd2c43178ab629332f6c401a6b2079799bf630..b19a742cae896eee751209234dd130535bb4cdf7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
@@ -20,9 +20,9 @@ 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_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
 .
 
@@ -40,7 +40,7 @@ fact vpushs_inv_atom_aux (M) (gv) (lv): is_model M →
 | #v #d #K #V #_ #_ #H destruct
 | #v #d #I #K #_ #_ #H destruct
 | #v1 #v2 #L #_ #Hv12 #IH #H destruct
-  /3 width=3 by veq_trans/ 
+  /3 width=3 by veq_trans/
 ]
 qed-.
 
@@ -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 →
@@ -92,7 +92,7 @@ lemma vpushs_inv_abst (M) (gv) (lv): is_model M →
 
 fact vpushs_inv_unit_aux (M) (gv) (lv): is_model M →
                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
-                                        ∀I,K. K.ⓤ{I} = L →
+                                        ∀I,K. K.ⓤ[I] = L →
                                         ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
 #M #gv #lv #HM #y #L #H elim H -y -L
 [ #Z #Y #H destruct
@@ -107,14 +107,14 @@ fact vpushs_inv_unit_aux (M) (gv) (lv): is_model M →
 qed-.
 
 lemma vpushs_inv_unit (M) (gv) (lv): is_model M →
-                                     ∀y,I,K. K.ⓤ{I} ⨁{M}[gv] lv ≘ y →
+                                     ∀y,I,K. K.ⓤ[I] ⨁{M}[gv] lv ≘ y →
                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
 /2 width=4 by vpushs_inv_unit_aux/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma vpushs_fwd_bind (M) (gv) (lv): is_model M →
-                                     ∀y,I,K. K.ⓘ{I} ⨁{M}[gv] lv ≘ y →
+                                     ∀y,I,K. K.ⓘ[I] ⨁{M}[gv] lv ≘ y →
                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
 #M #gv #lv #HM #y * [ #I | * #V ] #L #H
 [ /2 width=2 by vpushs_inv_unit/