lemma trivial_imp_no_distinct, no_distinct_imp_trivial; section structure
lemma list_comp_eq_set_comp
1. simplified runiq_alt: stripped unnecessary x ∈ Domain R prerequisite
2. with 1. simplified runiq_wrt_eval_rel
3. with 1. simplified disj_Un_runiq
4. with 1. simplified eval_runiq_rel
5. renamed fun sup_rels_from → sup_rels_from_alg, introduced definition sup_rels_from (the same for sets); sup_rels_from_paper_equiv_alg proves equivalence
6. simplified injections_paste
7. simplified injections_equiv