(* Forward lemmas with free variables inclusion for restricted closures *****)
(* Note: "⦃L2, T1⦄ ⊆ ⦃L2, T0⦄" does not hold *)
-(* Note: Take L0 = K0.â\93\93(â\93\9dW.V), L2 = K0.â\93\93W, T0 = #0, T1 = â¬\86*[1]V *)
+(* Note: Take L0 = K0.â\93\93(â\93\9dW.V), L2 = K0.â\93\93W, T0 = #0, T1 = â\87§*[1]V *)
(* Note: This invalidates rpxs_cpx_conf: "∀h, G. s_r_confluent1 … (cpx h G) (rpxs h G)" *)
lemma rpx_cpx_conf_fsge (h) (G): ∀L0,T0,T1. ⦃G,L0⦄ ⊢ T0 ⬈[h] T1 →
∀L2. ⦃G,L0⦄ ⊢⬈[h,T0] L2 → ⦃L2,T1⦄ ⊆ ⦃L0,T0⦄.