X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_compose_tls.ma;h=7d678a7f304117e6fc996f224a1fe8bc8f9967da;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=1a7947f382aa0b1944d8f6680274278d1be84d02;hpb=01b17de504f0049c15eadcdad651a19adaa954f7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
index 1a7947f38..7d678a7f3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
@@ -21,13 +21,10 @@ include "ground/arith/nat_rplus_pplus.ma".
 
 (* Advanced constructions with stream_tls ***********************************)
 
-lemma tr_compose_tls (i) (f2) (f1):
-      (⇂*[f1@❨i❩]f2)∘⇂*[i]f1 = ⇂*[i](f2∘f1).
-#i elim i -i
-[ #f2 * #p1 #f1 //
-| #i #IH #f2 * #p1 #f1
-  >nsucc_inj <stream_tls_swap <stream_tls_swap
-  <tr_pap_succ >nrplus_inj_dx >nrplus_inj_sn
-  <tr_compose_unfold <IH -IH //
-]
+lemma tr_compose_tls (p) (f1) (f2):
+      (⇂*[f1＠⧣❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
+#p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
+<tr_compose_unfold <tr_pap_succ
+>nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
+<IH -IH >nrplus_inj_dx >nrplus_inj_sn <stream_tls_plus //
 qed.