Lemma factor_dep_through_squash {X} {Q:∥ X ∥->UU} : (∏ h, isaprop (Q h)) -> (∏ x, Q(squash_element x)) -> (∏ h, Q h). Proof. intros i f ?. apply (h (make_hProp (Q h) (i h))). intro x. simpl. induction (squash_uniqueness x h). exact (f x). Defined.