(*
(* Basic_2A1: was: cpx_lleq_conf *)
lemma cpx_lfeq_conf: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
- â\88\80L1. L2 â\89¡[T1] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h] T2.
+ â\88\80L1. L2 â\89\98[T1] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h] T2.
/3 width=3 by lfeq_cpx_trans, lfeq_sym/ qed-.
*)
(* Basic_2A1: was: cpx_lleq_conf_sn *)
(*
(* Basic_2A1: was: cpx_lleq_conf_dx *)
lemma cpx_lfeq_conf_dx: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
- â\88\80L1. L1 â\89¡[T1] L2 â\86\92 L1 â\89¡[T2] L2.
+ â\88\80L1. L1 â\89\98[T1] L2 â\86\92 L1 â\89\98[T2] L2.
/4 width=6 by cpx_lfeq_conf_sn, lfeq_sym/ qed-.
*)
\ No newline at end of file