{A : Type} `{HasEquivs A} (a b : A) : (a = b) -> (a $<~> b). Proof. intros []; reflexivity. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.