experiment with dependent squashing...

proved

Lemma squash_to_set (X Y:UU) : forall f : X -> Y, isaset Y -> (forall x x' : X, f x == f x') -> squash_dep X -> Y.