X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_rmap_closed.ma;h=9e8a3a99ebdabe030c9de7c331fe104717e9d0e9;hb=d108bcea8ebae11b03e8d8a155dfd3f2eb445127;hp=ec386108eded9b3ab11c994a8d6b8fd0fa6d70d4;hpb=4939d8280cb3467cd8fa648b1cea04f74d71e8b7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
index ec386108e..9e8a3a99e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
@@ -59,7 +59,8 @@ qed-.
 
 lemma nap_plus_lift_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
       q ϵ 𝐂❨o,n❩ →
-      🠢[f](p)＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩ = 🠢[f](p●𝗟◗q)＠§❨m+n❩.
+      🠢[f]p＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩ = 🠢[f](p●𝗟◗q)＠§❨m+n❩.
 #o #f #p #q #m #n #Hq
+<tr_nap_plus_dx_xap
 /4 width=2 by eq_f2, tr_xap_eq_repl, tls_succ_lift_rmap_append_closed_Lq_dx/
 qed-.