lemma injections_paste: one direction of proof finished (needs clean-up though)
made Union_member work in both directions
finished proof of lemma injections_paste, and thus all dependencies of theorem injections_equiv