-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):