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=c117394ff52a03ca59887bd3dff0dc9c6652ee11;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=f9a9afa880298d3930ab0851adee9d78c2f8d0b2;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;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 f9a9afa88..c117394ff 100644
--- a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs.ma
@@ -51,7 +51,7 @@ lemma rexs_pair: ∀R. (∀L. reflexive … (R L)) →
 /3 width=5 by rex_pair, rexs_step_dx, inj/
 qed.
 
-lemma rexs_unit: ∀R,f,I,L1,L2. 𝐈❪f❫ → L1 ⪤[cext2 R,cfull,f] L2 →
+lemma rexs_unit: ∀R,f,I,L1,L2. 𝐈❨f❩ → L1 ⪤[cext2 R,cfull,f] L2 →
                  L1.ⓤ[I] ⪤*[R,#0] L2.ⓤ[I].
 /3 width=3 by rex_unit, inj/ qed.