scheme :: STACKS_1:sch 3
INDsch{ F1() -> StackAlgebra, F2() -> stack of F1(), P1[ set ] } :
P1[F2()]
provided
A1: for s being stack of F1() st emp s holds
P1[s] and
A2: for s being stack of F1()
for e being Element of F1() st P1[s] holds
P1[ push (e,s)]