proposition: Lemma hset_pi {A} `{H : IsHSet A} (x y : A) (p q : x = y) (r : p = q) : is_hset p q = r.
proof: Proof. red in H. pose (hprop_hset (H x y)). apply i. Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Classes HoTT.Basics.Trunc