:: deftheorem CPI defines -context_pos_in MSAFREE5:def 26 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
for b₇ being Nat holds
( b₇ = x -context_pos_in p iff p . b₇ is context of x );