//axioms
axiom @reflexive a. [True] = a == a;
//The reflexive axiom simply asserts referential transparency
//Not all LSTS preludes are referentially transparent

//TODO FIXME introduce syntax that would permit symmetric and transitive definition
//axiom @symmetric a, b. [True] = a == b => b == a;
//axiom @transitive a, b, c. [True] = a == b && b == c => a == c;