scheme :: TREES_2:sch 1
TreeStructInd{ F₁() -> Tree, P₁[ set ] } :

for t being Element of F₁() holds P₁[t]

provided

A1: P₁[ {} ] and
A2: for t being Element of F₁()
for n being Nat st P₁[t] & t ^ <*n*> in F₁() holds
P₁[t ^ <*n*>]