pub open spec fn transitive<T>(r: FnSpec<(T, T), bool>) -> bool
{ forall |x: T, y: T, z: T| #[trigger] r(x, y) && #[trigger] r(y, z) ==> r(x, z) }