fact: Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q) : id_sym p = id_sym q := ap (@id_sym _ _ _) h.
imports: Unicode.Utf8 Coq.Program.Tactics Setoid Relations Equations.Type.All CRelationClasses CMorphisms