lemma elem_in_eq_class, and used that to simplify lemma elem_in_uniq_eq_class
lemma diff_elem_in_eq_class
lemma Range_except_irrelevant
lemma Domain_except (using Range_except)
new introduction rule injectionsI, and used that to simplify some proofs
split some ↔ lemmas into both directions for better reusability:
* runiq_alt: runiq_imp_triv_singleton_Im, triv_singleton_Im_imp_runiq
* runiq_basic: runiq_imp_uniq_right_comp, uniq_right_comp_imp_runiq
new lemmas:
* runiq_wrt_ex1: runiq_imp_ex1_right_comp, ex1_right_comp_imp_runiq
* runiq_wrt_THE: runiq_imp_THE_right_comp, THE_right_comp_imp_runiq
* runiq_conv_wrt_THE: runiq_conv_imp_THE_left_comp, THE_left_comp_imp_runiq_conv
* runiq_relation_except_singleton
further progress in proof of lemma wd_outcome