/* * Between finite sets of the same size, total injections are bijections. */ MACHINE InjBij ASSERTIONS !(ss, tt) . (ss : FIN(INTEGER) & tt : FIN(INTEGER) & card(ss) = card(tt) => (ss >-> tt) <: (ss >->> tt)) END