pub open spec fn commutative_foldr<A, B>(f: FnSpec<(A, B), B>) -> bool
{ forall |x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v)) }