-(* 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