ToProve.het revision 21b2c993ba4467ad14509265270ad71ef59c4064
logic CommonLogic
spec ToProve =
. (P x)
(and (P x) (Q y))
. (Q y) %implied
. (P y) %implied
end