/2 width=5 by rex_dropable_dx/ qed-.
lemma rdeq_inv_lifts_bi: âL1,L2,U. L1 â[U] L2 â âb,f. đâŚf⌠â
- âK1,K2. âŹ*[b, f] L1 â K1 â âŹ*[b, f] L2 â K2 â
+ âK1,K2. âŹ*[b,f] L1 â K1 â âŹ*[b,f] L2 â K2 â
âT. âŹ*[f] T â U â K1 â[T] K2.
/2 width=10 by rex_inv_lifts_bi/ qed-.