ParameterSpecTest.het revision 2937d25c9a98c4c1c17df12cb1ac61f8ce638b21
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]
end