`{Contr A} (x y : A) : x = y := (contr x)^ @ (contr y). Global Instance contr_paths_contr `{Contr A} (x y : A) : Contr (x = y) | 10000. Proof. apply (Build_Contr _ ( x y)). intro r; destruct r; apply concat_Vp. Defined.
Require Import Overture PathGroupoids.