(* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *)
lemma rdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ≛[T] K2 →
- â\88\80b,f. â¬\87*[b,f] L1 â\89\98 K1 â\86\92 â¬\87*[b,f] L2 ≘ K2 →
- â\88\80U. â¬\86*[f] T ≘ U → L1 ≛[U] L2.
+ â\88\80b,f. â\87©*[b,f] L1 â\89\98 K1 â\86\92 â\87©*[b,f] L2 ≘ K2 →
+ â\88\80U. â\87§*[f] T ≘ U → L1 ≛[U] L2.
/3 width=9 by rex_lifts_bi, tdeq_lifts_sn/ qed-.
(* Forward lemmas with length for local environments ************************)