proposition: Lemma squash_rec {X : UU} (P : ∥ X ∥ -> hProp) : (∏ x, P (hinhpr x)) -> (∏ x, P x).
proof: Proof. intros xp x'. simple refine (hinhuniv _ x'). intro x. assert (q : hinhpr x = x'). { apply propproperty. } induction q. exact (xp x). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions