#5 Too restrictive: Not all inductive cases are covered

[Son Hoang]

In the attached example, a Stack datatype is defined inductively:
STACK(S) = EmptyStack |
Push(top:S, rest: STACK(S))
An operator top(s : STACK) is defined with well-definedness condition "s != EmptyStack)
top is defined recursively
top(Push(t,r)) = t

However, an error is "Not all inductive cases are covered" for the theory.
This is too restrictive since the well-definedness condition guarantees that all cases are covered for any well-defined input.

Son