update in groud_2 and models

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

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma
index 8d59fe006d913b5c34454e5aaa71c494a9d2216a..30d7d60d2beb3b156977b490c7520044d08db0e9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma
@@ -81,3 +81,15 @@ qed-.
 lemma li_inv_unit (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓤ{I}⟧{M}[gv] →
                             ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
 /2 width=4 by li_inv_unit_aux/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma li_fwd_bind (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓘ{I}⟧{M}[gv] →
+                            ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
+#m #gv #v * [ #I | * #V ] #L #H
+[ @(li_inv_unit … H)
+| elim (li_inv_abbr … H) -H #lv #d #Hl #_ #Hv
+  /2 width=4 by ex2_2_intro/
+| @(li_inv_abst … H)
+]
+qed-.