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=59f9b3e84fa4a49b717fcf69c9693e0f09650c1f;hp=7f5eacc47417d5b1e481d016c73875a66aab2d8b;hb=cc600ed1e115d5566947288d532a1e89d989227f;hpb=ea918ec7701db4458c5ca25885e80abc6fed1be7

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 7f5eacc47..59f9b3e84 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma
@@ -20,9 +20,9 @@ include "apps_2/models/vpushs.ma".
 (* Properties with fold for restricted closures *****************************)
 
 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].
+                       ∀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].
 #M #H1M #H2M #L elim L -L [| #K * [| * ]]
 [ #T1 #T2 #gv #lv #H12
   >fold_atom >fold_atom
@@ -34,7 +34,7 @@ lemma vpushs_fold (M): is_model M → is_extensional M →
   >fold_pair >fold_pair
   @IH -IH #v #Hv
   @(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ]
-  /4 width=1 by vpushs_abbr, mr/
+  /4 width=1 by vpushs_abbr, mc, mr/
 | #W #IH #T1 #T2 #gv #lv #H12
   >fold_pair >fold_pair
   /5 width=1 by vpushs_abst, mx, mr/
@@ -43,10 +43,10 @@ qed.
 
 (* Inversion lemmas with fold for restricted closures ***********************)
 
-lemma vpushs_inv_fold (M): is_model 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].
-#M #HM #L elim L -L [| #K * [| * ]]
+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].
+#M #H1M #H2M #L elim L -L [| #K * [| * ]]
 [ #T1 #T2 #gv #lv
   >fold_atom >fold_atom #H12 #v #H
   lapply (vpushs_inv_atom … H) -H // #Hv
@@ -60,7 +60,8 @@ lemma vpushs_inv_fold (M): is_model M →
   >fold_pair >fold_pair #H12 #y #H
   elim (vpushs_inv_abbr … H) -H // #v #Hlv #Hv
   lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12
-  /4 width=7 by ti_comp, veq_refl, md, mq/
+  @(mq … H1M) [4,5: @(ti_comp … Hv) /3 width=2 by veq_refl/ |1,2: skip ]
+  /4 width=7 by ti_comp, ti_fwd_abbr_dx, veq_refl, mq/
 | #W #IH #T1 #T2 #gv #lv
   >fold_pair >fold_pair #H12 #y #H
   elim (vpushs_inv_abst … H) -H // #v #d #Hlv #Hv