-* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex7_5_intro โฆ (๐ ก[f]p) (๐ ก[๐ ข[f](pโ๐)]b) (๐ ก[๐ ข[f](pโ๐โbโ๐)]q) (๐ ข[f](pโ๐โb)๏ผ โจmโฉ) (๐ ข[f](pโ๐โbโ๐โq)๏ผ ยงโจnโฉ))
-[ -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
-| -Hb -Hm -Hn -Ht1 -Ht2
- /2 width=1 by lift_path_guard/
-| -Hp -Hm -Hn -Ht1 -Ht2 //
-| -Hp -Hb -Hn -Ht1 -Ht2
+* #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