prove_abs_fn_onto : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Proves that a type abstraction function is onto (surjective).
DESCRIPTION
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))
then prove_abs_fn_onto th proves from this theorem that the function abs is onto, returning the theorem: 
   |- !a. ?r. (a = abs r) /\ P 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_one_one, prove_rep_fn_one_one, prove_rep_fn_onto
HOL  Kananaskis-14