add a lemma to simplify a proof

Lemma factor_dep_through_squash {X:UU} {Q:squash X->UU} :
  (forall y, isaprop (Q y)) ->
  (forall x, Q(squash_element x)) ->
  (forall h, Q h).