pred_ex_Sn lemma complete and deleted some dead proof code

Fixed/updated the pred_ex_Sn proof w/ Jay's recommendations (the proof
which provides the predecessor of a Node on a strand (assuming of
course it is node Node 0 on that strand)).

Also deleted some no longer in use tactics/statements from the
"bundle_minimal_ex" proof (as I was working I pushed this code down and
began working above it… and didn't need/come back to it)
bundle_minimal_ex proven, given finite_rev_path_end

I proved all finite subsets in a bundle have a minimal member, given
that any backwards EdgePathEq eventually dead ends. This shouldn't be
too difficult to prove… just showing a path with only finitely many
possible members (which is not acyclic) eventually must end.

Also made the edge/path definitions for nodes in a specified set have a
more consistent constructor naming scheme.

And… deleted some dead/useless code/proofs.