-theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 Ο΅ π β
- t1 β‘ππ[p,q] t2 β βΌ[f]t1 β‘π’π[βp,βq] βΌ[f]t2.
-#f #p #q #t1 #t2 #H0t1
-* #n * #H1n #Ht1 #Ht2
-@(ex_intro β¦ (ββq)) @and3_intro
-[ -H0t1 -Ht1 -Ht2
- >structure_L_sn >structure_reverse
- >H1n in β’ (??%?); >path_head_structure_depth <H1n -H1n //
+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/