fact: Definition function_inverse {X Y:Type} (f:X->Y) (i:invertible f) : { g:Y->X | (forall x:X, g (f x) = x) /\ (forall y:Y, f (g y) = y) } := (constructive_definite_description _ (unique_inverse f i)).
imports: Image Description FunctionalExtensionality