injective_on

vstd::relations

Function injective_on 

Source 
pub open spec fn injective_on<X, Y>(r: FnSpec<(X,), Y>, dom: Set<X>) -> bool
Expand description
{
    forall |x1: X, x2: X| {
        dom.contains(x1) && dom.contains(x2) && #[trigger] r(x1) == #[trigger] r(x2)
            ==> x1 == x2
    }
}