#h #o #G #L #T2 #T0 #HT20 #T1 #HT01
elim (cpx_tdeq_conf … HT01 T2) -HT01 /3 width=3 by tdeq_sym, ex2_intro/
qed-.
(* Basic_2A1: uses: cpx_lleq_conf *)
lemma cpx_lfdeq_conf: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
#h #o #G #L #T2 #T0 #HT20 #T1 #HT01
elim (cpx_tdeq_conf … HT01 T2) -HT01 /3 width=3 by tdeq_sym, ex2_intro/
qed-.
(* Basic_2A1: uses: cpx_lleq_conf *)
lemma cpx_lfdeq_conf: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →