λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / i_static / rexs.ma

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 a53ee2c823636520601d31342a6210a725efc554..58b26cd7621c57bfd425958afe5488e2d2aafc6b 100644 (file)
--- 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)) →