Revision of structure theorems (1)

* ~ressunif moved up
* ~imasvalstr: comment corrected
*  ~prdsvallem: name adjusted to ~prdsbaslem
* ~prdsvallem: extracted from proof of ~prdsval and revised (Dependeny on ~df-hom removed).
* ~prdsval, proof shortened,
* ~rescco, ~0pos: proof shortened, dependency on df-* and *ndx removed
* ~ edgfndx: added (for uniformity reasons)
* ~ edgfndxnn: proof shortened