proposition: Theorem equiv_hprop_allpath `{Funext} (A : Type) : IsHProp A <~> (forall (x y : A), x = y).
proof: Proof. rapply (equiv_iff_hprop (@path_ishprop A) (@hprop_allpath A)). apply hprop_allpath; intros f g. funext x y. pose (C := Build_Contr A x (f x)). apply path_contr. Defined.
imports: HoTT.Basics HoTT.Types