+lemma ibfr_structure_unwind_bi (f) (t1) (t2) (r):
+ ▼[⫯𝐢]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯𝐢]t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
+#f #t1 #t2 #r #Ht12
+lapply (ibfr_lift_bi (f) … Ht12) -Ht12
+<lift_path_structure #Ht12
+@(ibfr_eq_repl … Ht12) -r
+@(subset_eq_canc_dx … (lift_unwind2_term_after …))
+@unwind2_term_eq_repl_sn -t1 -t2 //
+qed-.
+
+lemma ibfr_unwind_bi_push (f) (t1) (t2) (r):