pub open spec fn injective<X, Y>(r: FnSpec<(X,), Y>) -> bool
{ forall |x1: X, x2: X| #[trigger] r(x1) == #[trigger] r(x2) ==> x1 == x2 }