Function predicate_syntactic_eq 

pub fn predicate_syntactic_eq(a: &Spanned<Expr>, b: &Spanned<Expr>) -> bool

Structural equality on Aver predicate expressions with commutator relaxation: at every BinOp comparator node, allow the operands + operator to be swapped. Both a >= 0 and 0 <= a compare equal, recursively. Non-comparator BinOps (Add, Sub, …) and other Expr variants fall through to the derived PartialEq on Spanned<Expr> (which compares .node only — line numbers don’t participate). Used by the when-vs-refinement-invariant identity check so a redundantly-written user when gets recognised even when the operand order doesn’t match the smart constructor’s predicate verbatim.