proposition: Lemma hprop_hset {A} (h : HProp A) : HSet A.
proof: Proof. intro x. set (g y := h x y). intros y z w. assert (forall y z (p : y = z), p = id_trans (id_sym (g y)) (g z)). intros. apply id_trans_sym. destruct (apd_eq p (g y0)). apply apd. rewrite X. now rewrite (X _ _ z). Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes