ParameterSpecTest.het revision e822de03185f78e7735471f31b1dd113d6b6fdd8
library ParameterSpecTest
spec X =
sort sX
pred A : sX *sX
end
spec Sym [sort s pred p1:s*s] =
forall x,y:s
. p1(x,y) <=> p1(y,x)
end
spec X_inv =
Sym [X fit p1 |-> A]
end