update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
index acc891d4bf1e1158c25e061ef4d8c0b1b4c01393..ec92283789ce8f9b08ebbd383b7c68cf82cf6461 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
@@ -61,7 +61,7 @@ qed-.
 (*** compose_inv_S1 *)
 lemma tr_compose_inv_next_sn (f2) (f1):
       ∀f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
-      ∧∧ ↑(f2@❨p1❩) = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+      ∧∧ ↑(f2＠⧣❨p1❩) = p & f2∘(p1⨮f1) = f2＠⧣❨p1❩⨮f.
 #f2 #f1 #f #p1 #p
 <tr_compose_unfold #H destruct
 /2 width=1 by conj/