(* Forward lemmas with free variables inclusion for restricted closures *****)
(* Note: "⦃L2, T1⦄ ⊆ ⦃L2, T0⦄" does not hold *)
(* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⬆*[1]V *)
(* Note: This invalidates lfpxs_cpx_conf: "∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G)" *)
(* Forward lemmas with free variables inclusion for restricted closures *****)
(* Note: "⦃L2, T1⦄ ⊆ ⦃L2, T0⦄" does not hold *)
(* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⬆*[1]V *)
(* Note: This invalidates lfpxs_cpx_conf: "∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G)" *)