\DOC prove_abs_fn_one_one

\TYPE {prove_abs_fn_one_one : (thm -> thm)}

\SYNOPSIS
Proves that a type abstraction function is one-to-one (injective).

\DESCRIBE
If {th} is a theorem of the form returned by the function
{define_new_type_bijections}:
{
   |- (!a. abs(rep a) = a) /\ (!r. P r = (rep(abs r) = r))
}
\noindent then {prove_abs_fn_one_one th} proves from this theorem that the
function {abs} is one-to-one for values that satisfy {P}, returning the
theorem:
{
   |- !r r'. P r ==> P r' ==> ((abs r = abs r') = (r = r'))
}
\FAILURE
Fails if applied to a theorem not of the form shown above.

\SEEALSO
new_type_definition, define_new_type_bijections, prove_abs_fn_onto,
prove_rep_fn_one_one, prove_rep_fn_onto.

\ENDDOC