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