There was an error while loading. Please reload this page.
=*=
The predicate for behavioral equivalence, written =*=, is a binary operator defined on each hidden sort.