fact: Definition path_contr {A} {H:Contr A} (x y : A) : x = y := concat (id_sym (@contr _ H x)) (@contr _ H y).
imports: Unicode.Utf8 Coq.Program.Tactics Setoid Relations Equations.Type.All CRelationClasses CMorphisms