documented runiq_basic
new lemma restrict_ext