open INV
-- arbitrary objects
  op s : -> Sys .
-- check
  red inv10(s) implies inv1(s) .
close