proposition: Corollary iff_contr_hprop (A : Type) `{IsHProp A} : Contr A <-> A.
proof: Proof. split. - apply center. - rapply contr_inhabited_hprop. Defined.
imports: Basics.Overture Basics.Contractible Basics.Equivalences Basics.Tactics Basics.Nat