Progress on [isconn_wedge_incl].
Completed crude proof of wedge-elim, modulo lemma on connectedness of point-inclusion.