lemma_injective_implies_injective_on

vstd_extra::function_properties

Function lemma_injective_implies_injective_on 

Source 
pub proof fn lemma_injective_implies_injective_on<T, U>(
    f: FnSpec<(T,), U>,
    dom: Set<T>,
)
Expand description
requires
injective(f),
ensures
injective_on(f, dom),

A function is injective on the whole type implies that it is injective on any sub-domain.