proposition: Lemma hset_hprop : forall X : Type, IsHProp X -> IsHSet X.
proof: Proof. intros X H. assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z). { intros. unfold eq_trans, eq_ind. destruct p. reflexivity. } assert (forall (x y z:X) (p : y = z), p = eq_trans (eq_sym (H x y)) (H x z)). { intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind. destruct p, (H x y). reflexivity. } intros x y p q. rewrite (H1 x x y p), (H1 x x y q). reflexivity. Qed.
imports: Coq.Logic.FunctionalExtensionality