So, I have two functions, $f:X \to Y$ and $g: Y \to X$, and I want to express the proposition that they are inverses of each other.
The classical way to do this is showing that $\forall x\in X \ldotp g(f(x))=x$, and that $\forall y \in Y \ldotp f(g(y)) = y$.
However, I'm using these in an SMT setting, and for technical reasons, I can only quantify over the set $X$, not $Y$.
I'm wondering, is there some proposition $P(x,f,g)$ I can use, where $f$ and $g$ are inverses of each other, if and only if $\forall x \in X \ldotp P(x,f,g)$?
EDIT: I had an extra function application in each condition, thanks @yanko