-(* COMMENT
-axiom pippo (b) (q) (n):
- ↑❘q❘ = (↑[q]𝐢)@❨n❩ →
- ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩.
-
-lemma unwind_rmap_tls_eq_id (p) (n):
- ❘p❘ = ↑[p]𝐢@❨n❩ →
- (𝐢) ≗ ⇂*[n]↑[p]𝐢.
-#p @(list_ind_rcons … p) -p
-[ #n <depth_empty #H destruct
-| #p * [ #m ] #IH #n
- [ <depth_d_dx <unwind_rmap_pap_d_dx #H0
- @(stream_eq_trans … (unwind_rmap_tls_d_dx …))
- @(stream_eq_trans … (IH …)) -IH //
- | /2 width=1 by/
- | <depth_L_dx <unwind_rmap_L_dx
- cases n -n [| #n ] #H0
- [
- |
- ]
- | /2 width=1 by/
- | /2 width=1 by/
- ]
-]
-
-
-(* (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢@❨n+❘b❘❩ *)
-(* [↑[p]𝐢@❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
-lemma unwind_rmap_tls_eq (f) (p) (n):
- ❘p❘ = ↑[p]𝐢@❨n❩ →
- f ≗ ⇂*[n]↑[p]f.
-#f #p #n #Hp
-@(stream_eq_canc_dx … (stream_tls_eq_repl …))
-[| @unwind_rmap_decompose | skip ]
-<tr_compose_tls <Hp