lemma ibfr_eq_canc_sn (t) (t1) (t2) (r):
t ⇔ t1 → t ➡𝐢𝐛𝐟[r] t2 → t1 ➡𝐢𝐛𝐟[r] t2.
#t #t1 #t2 #r #Ht1
-* #p #b #q #m #n #Hr#Hp #Hb #Hm #Hn #Ht #Ht2 destruct
-@(ex7_5_intro … Hp Hb Hm Hn) [ // ] -Hp -Hb -Hm -Hn
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht #Ht2 destruct
+@(ex6_5_intro … p … Hb Hm Hn) [ // ] -Hb -Hm -Hn
[ /2 width=3 by subset_in_eq_repl_back/
| /5 width=3 by subset_eq_canc_sn, fsubst_eq_repl, lift_term_eq_repl_dx, grafted_eq_repl/
]