#h #n1 #G #L #T1 #HT1 #T2 #HT12 #n2 #T3 #HT23
/4 width=5 by cpms_trans, tweq_canc_sn/
qed-.
lemma cnuw_dec_ex (h) (G) (L):
∀T1. ∨∨ ❪G,L❫ ⊢ ➡𝐍𝐖*[h] T1
#h #n1 #G #L #T1 #HT1 #T2 #HT12 #n2 #T3 #HT23
/4 width=5 by cpms_trans, tweq_canc_sn/
qed-.
lemma cnuw_dec_ex (h) (G) (L):
∀T1. ∨∨ ❪G,L❫ ⊢ ➡𝐍𝐖*[h] T1