fact: Definition moveR_E A B (f:A -> B) {H : IsEquiv f} (x : A) (y : B) (p : x = f^^-1 y) : (f x = y) := ap f p @ (@eisretr _ _ f _ y).
imports: Unicode.Utf8 Coq.Program.Tactics Setoid Relations Equations.Type.All CRelationClasses CMorphisms