lemma csx_fpbq_conf: ∀h,G1,L1,T1. ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
∀G2,L2,T2. ⦃G1,L1,T1⦄ ≽[h] ⦃G2,L2,T2⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
lemma csx_fpbq_conf: ∀h,G1,L1,T1. ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
∀G2,L2,T2. ⦃G1,L1,T1⦄ ≽[h] ⦃G2,L2,T2⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *