update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_uni_compose.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
index 3d329e795f23b79be89abb02e386945bdaed02e5..54cf97875272b3995f5bea6b84279ae21f3ec9d4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
@@ -45,7 +45,7 @@ qed.
 (* Main constructions with tr_compose and tr_tls ****************************)
 
 theorem tr_compose_uni_dx (f) (p):
-        (𝐮❨f@❨p❩❩∘⇂*[p]f ≗ f∘𝐮❨p❩).
+        (𝐮❨f@❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
 #f #p
 @nstream_eq_inv_ext #q
 <tr_compose_pap <tr_compose_pap