λδ-2B is released

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

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma
index b3ad3915733a01f5e97978b1f0cd49ade8bc0292..6975017c595632d885aa7cf4c99997623153a54d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma
@@ -31,7 +31,7 @@ interpretation "local environment interpretation (model)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact li_inv_abbr_aux (M) (gv): is_model M → 
+fact li_inv_abbr_aux (M) (gv): is_model M →
                                ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV →
                                ∃∃lv. lv ϵ ⟦L⟧[gv] & ⫯[0←⟦V⟧[gv,lv]]lv ≗ v.
 #M #gv #HM #v #Y #H elim H -v -Y