:: deftheorem defines still_not-bound_in QC_LANG1:def 29 :
for A being QC-alphabet
for ll being FinSequence of QC-variables A holds still_not-bound_in ll = { (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } ;