Thanks everyone. I'd like to close the question.
Yesterday I've done a formal proof by constructing an explicit mapping from
the finite set to infinite set (using the Hilbert @ operator), then use
IN_INFINITE_NOT_FINITE to assert the existence of elements from the rest of
infinite map. I also rec
Yesterday I wanted to change the definition of my datatype to support
summing over a set of values of the same type:
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| summ (CCS set) (num set)`;
if so, then the original binary "sum" will become the new summ operator
ov
