E.2.4 COMPOUND_SYMBOLS_ARE_NICE

spec

Compound_Symbols_Are_Nice =

 

List_With_Order[ Natural fit Elem |-> Nat,  __<__ |-> __leq__ ]

and

 

List_With_Order[ Natural fit Elem |-> Nat,  __<__ |-> __geq__ ]

then

var

l : List[Nat]

axiom

order[__geq__](l) = reverse(order[__leq__](l))

end