undid one proof step simplification that didn't work
corollary Domain_outside_singleton, lemma Range_outside_sub
thus simplified injections_paste proof
documented definition injective, lemma runiq_and_conv_imp_injective
got rid of some metis invocations