-lemma lpx_cpx_conf_fsge (h) (G): ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
- ∀L2. ⦃G, L0⦄ ⊢ ⬈[h] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄.
-/3 width=4 by lfpx_cpx_conf_fsge, lpx_lfpx/ qed-.
+lemma lpx_cpx_conf_fsge (G):
+ ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈ T1 →
+ ∀L2. ❪G,L0❫ ⊢ ⬈ L2 → ❪L2,T1❫ ⊆ ❪L0,T0❫.
+/3 width=4 by rpx_cpx_conf_fsge, lpx_rpx/ qed-.