-(* (โโ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
-
-@(stream_eq_canc_dx) โฆ (unwind_rmap_decompose โฆ))
-
-*)
-lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ฯต ๐ โ
- t1 โก๐๐[p,q] t2 โ โผ[๐ข]t1 โก๐[โp,โq] โผ[๐ข]t2.
-#p #q #t1 #t2 #H0t1
-* #b #n * #Hb #Hn #Ht1 #Ht2
-@(ex1_2_intro โฆ (โb) (โโญโq)) @and4_intro
-[ //
-| (*//*)
-| lapply (in_comp_unwind_bi (๐ข) โฆ Ht1) -Ht1 -H0t1 -Hb -Ht2
- <unwind_path_d_empty_dx <depth_structure //
-| lapply (unwind_term_eq_repl_dx (๐ข) โฆ Ht2) -Ht2 #Ht2
+theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ฯต ๐ โ
+ t1 โก๐๐[r] t2 โ โผ[f]t1 โก๐ข๐[โr] โผ[f]t2.
+#f #t1 #t2 #r #H0t1
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro โฆ (โp) (โq) (โญq))
+[ -H0t1 -Hn -Ht1 -Ht2 //
+| -H0t1 -Ht1 -Ht2
+ /2 width=2 by path_closed_structure_depth/
+| lapply (in_comp_unwind2_path_term f โฆ Ht1) -Ht2 -Ht1 -H0t1
+ <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
+ <nap_unwind2_rmap_append_closed_Lq_dx_depth //
+| lapply (unwind2_term_eq_repl_dx f โฆ Ht2) -Ht2 #Ht2