proposition: Lemma squash_uniqueness {X} (x:X) (h:∥ X ∥) : squash_element x = h.
proof: Proof. intros. apply propproperty. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions