proposition: Lemma factor_dep_through_squash {X} {Q:∥ X ∥->UU} : (∏ h, isaprop (Q h)) -> (∏ x, Q(squash_element x)) -> (∏ h, Q h).
proof: Proof. intros i f ?. apply (h (make_hProp (Q h) (i h))). intro x. simpl. induction (squash_uniqueness x h). exact (f x). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions