new lemma converse_empty
new lemma runiq_emptyrel; started work on lemma injections_exist