-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro โฆ (โ[f]p) (โ[โ[pโ๐โ๐]f]q) ((โ[pโ๐โ๐โq]f)๏ผ โงฃโจkโฉ))
-[ -H1k -Ht1 -Ht2 //
-| -Ht1 -Ht2
- <lift_rmap_L_dx >lift_path_L_sn
- <(lift_path_head_closed โฆ H1k) in โข (??%?); -H1k //
-| lapply (in_comp_lift_path_term f โฆ Ht1) -Ht2 -Ht1 -H1k
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro โฆ (๐ ก[f]p) (๐ ก[๐ ข[f](pโ๐)]b) (๐ ก[๐ ข[f](pโ๐โbโ๐)]q) (๐ ข[f](pโ๐โb)๏ผ โจmโฉ) (๐ ข[f](pโ๐โbโ๐โq)๏ผ ยงโจnโฉ))
+[ -Hb -Hm -Hn -Ht1 -Ht2 //
+| -Hm -Hn -Ht1 -Ht2 //
+| -Hb -Hn -Ht1 -Ht2
+ /2 width=1 by lift_path_closed/
+| -Hb -Hm -Ht1 -Ht2
+ /2 width=1 by lift_path_rmap_closed_L/
+| lapply (in_comp_lift_path_term f โฆ Ht1) -Ht2 -Ht1 -Hn