X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Fmodel_li.ma;h=30d7d60d2beb3b156977b490c7520044d08db0e9;hp=8d59fe006d913b5c34454e5aaa71c494a9d2216a;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hpb=f86ab1580e0bab7f8cada3cc7ffdf80f40e3de9a

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 8d59fe006..30d7d60d2 100644
--- 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-.