proposition: Lemma contr_inhabited_hprop (A : Type) `{H : IsHProp A} (x : A) : Contr A.
proof: Proof. apply (Build_Contr _ x). intro y. rapply center. Defined.
imports: Basics.Overture Basics.Contractible Basics.Equivalences Basics.Tactics Basics.Nat