deleted b.ll02 (was redundant with existing RelationProperties.trivial_subset)
moved b.ll05 → RelationProperties.runiq_singleton_rel; direct, straightforward proof
Note: Sledgehammer told me "by (metis equalityE the_elem_eq), but as equalityE is an inference rule and the_elem_eq is a simplification rule, I could break it down to by (rule equalityE) simp
moved unnamed lemma "trivial X ⇒ runiq X" to RelationProperties.runiq_trivial_rel
moved b.ll28 → RelationProperties.paste_outside_restrict
documented runiq_paste{1,2}
moved b.ll27 → ListUtils.set_concat; simplified proof:
* pattern matching with "is" instead of "let"
* using built-in inference rule for the two proof cases (note "proof" instead of "proof -")