X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_rmap_eq.ma;h=bf5151f00a852df4b855705ad94817cea27b2e88;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=a2f841e43456f83c320ec7d0489787ec80f14110;hpb=5c2d38b46908f662cbb717156b29101ff30f8352;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
index a2f841e43..bf5151f00 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
@@ -13,9 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/substitution/lift_rmap.ma".
-include "ground/relocation/tr_pn_eq.ma".
+include "delayed_updating/substitution/prelift_rmap_eq.ma".
 include "ground/lib/stream_tls_plus.ma".
-include "ground/lib/stream_tls_eq.ma".
 include "ground/arith/nat_plus_rplus.ma".
 include "ground/arith/nat_rplus_pplus.ma".
 
@@ -26,13 +25,8 @@ include "ground/arith/nat_rplus_pplus.ma".
 lemma lift_rmap_eq_repl (p):
       stream_eq_repl … (λf1,f2. ↑[p]f1 ≗ ↑[p]f2).
 #p elim p -p //
-* [ #k ] #p #IH #f1 #f2 #Hf
-[ /3 width=1 by stream_tls_eq_repl/
-| /2 width=1 by/
-| /3 width=1 by tr_push_eq_repl/
-| /2 width=1 by/
-| /2 width=1 by/
-]
+#l #p #IH #f1 #f2 #Hf
+/3 width=1 by prelift_rmap_eq_repl/
 qed.
 
 lemma tls_lift_rmap_d_dx (f) (p) (n) (k):