proposition: Theorem hprop_allpath (A : Type) : (forall (x y : A), x = y) -> IsHProp A.
proof: Proof. intros H; apply istrunc_S; intros x y. nrapply contr_paths_contr. exact (Build_Contr _ x (H x)). Defined.
imports: Basics.Overture Basics.Contractible Basics.Equivalences Basics.Tactics Basics.Nat