proposition: Lemma contr_equiv A {B} (f : A -> B) `{IsEquiv A B f} `{Contr A} : Contr B.
proof: Proof. apply (Build_Contr _ (f (center A))). intro y. apply moveR_equiv_M. apply contr. Defined.
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics