can't further reuse RelationProperties
TODO
TODO
changed statement of no_distinct_imp_trivial to a form that's easier to reason with
new lemma runiq_basic: completely elementary restatement of runiq