(* Basic_2A1: was just: lleq_lpx_trans *)
lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 →
∀L1. L1 ≡[h, o, T] L2 →
∃∃K1. ⦃G, L1⦄ ⊢ ⬈[h, T] K1 & K1 ≡[h, o, T] K2.
#h #o #G #T #L2 #K2 #HLK2 #L1 #HL12
elim (lfpx_lfdeq_conf … o … HLK2 L1)
(* Basic_2A1: was just: lleq_lpx_trans *)
lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 →
∀L1. L1 ≡[h, o, T] L2 →
∃∃K1. ⦃G, L1⦄ ⊢ ⬈[h, T] K1 & K1 ≡[h, o, T] K2.
#h #o #G #T #L2 #K2 #HLK2 #L1 #HL12
elim (lfpx_lfdeq_conf … o … HLK2 L1)