(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
lemma req_inv_lifts_bi: ∀L1,L2,U. L1 ≡[U] L2 → ∀b,f. 𝐔⦃f⦄ →
(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
lemma req_inv_lifts_bi: ∀L1,L2,U. L1 ≡[U] L2 → ∀b,f. 𝐔⦃f⦄ →