scheme :: MSAFREE5:sch 4
ContextInd{ P₁[ set ], F₁() -> non empty non void ManySortedSign , F₂() -> SortSymbol of F₁(), F₃() -> non-empty ManySortedSet of the carrier of F₁(), F₄() -> Element of F₃() . F₂(), F₅() -> context of F₄() } :

P₁[F₅()]

provided

A0: P₁[F₄() -term ] and
A1: for o being OperSymbol of F₁()
for w being Element of Args (o,(Free (F₁(),F₃()))) st w is F₄() -context_including & P₁[F₄() -context_in w] holds
for C being context of F₄() st C = o -term w holds
P₁[C]