matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq_etc.ma

   1
   2 include "delayed_updating/unwind1/unwind.ma".
   3 (*
   4 include "ground/relocation/tr_compose_compose.ma".
   5 include "ground/relocation/tr_compose_eq.ma".
   6 *)
   7 (* Advanced constructions with proj_rmap and stream_tls *********************)
   8 (* COMMENT
   9 lemma unwind_rmap_tls_d_dx (f) (p) (m) (n):
  10       ⇂*[m+n]▼[p]f ≗ ⇂*[m]▼[p◖𝗱n]f.
  11 #f #p #m #n
  12 <unwind_rmap_d_dx >nrplus_inj_dx
  13 /2 width=1 by tr_tls_compose_uni_dx/
  14 qed.
  15 *)