λδ-2B is released

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

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 8ac1699861e2c7751fcc34c38fd31e26d7bd645f..d017bc16a5950775b16fd35ef1c26ec2397736d5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma
@@ -21,7 +21,7 @@ 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]) → 
+                       (∀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