X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fi_static%2Frexs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fi_static%2Frexs.ma;h=58b26cd7621c57bfd425958afe5488e2d2aafc6b;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=a53ee2c823636520601d31342a6210a725efc554;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs.ma b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs.ma
index a53ee2c82..58b26cd76 100644
--- a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs.ma
@@ -101,7 +101,7 @@ lemma rexs_inv_sort: ∀R,Y1,Y2,s. Y1 ⪤*[R,⋆s] Y2 →
       /4 width=7 by ex3_4_intro, rexs_step_dx, or_intror/
     ]
   ]
-] 
+]
 qed-.
 
 lemma rexs_inv_gref: ∀R,Y1,Y2,l. Y1 ⪤*[R,§l] Y2 →
@@ -119,7 +119,7 @@ lemma rexs_inv_gref: ∀R,Y1,Y2,l. Y1 ⪤*[R,§l] Y2 →
       /4 width=7 by ex3_4_intro, rexs_step_dx, or_intror/
     ]
   ]
-] 
+]
 qed-.
 
 lemma rexs_inv_bind: ∀R. (∀L. reflexive … (R L)) →