% The builtin "-(-)" notation desugars to "\apply{-}{-}".
% This is just a dummy definition.
\begin{definition}\label{apply}
    $\apply{f}{x} = x$.
\end{definition}

% Dummy definition for the domain
\begin{definition}\label{dom}
    $\dom{f} = f$.
\end{definition}

% Dummy definition for right-uniqueness
\begin{definition}\label{rightunique}
    $f$ is right-unique iff $f=f$.
\end{definition}

% Dummy definition for relations
\begin{definition}\label{relation}
    $f$ is a relation iff $f=f$.
\end{definition}

\begin{proposition}\label{definefunctiontest}
    If $x\in y$, then $x\in y$.
\end{proposition}
\begin{proof}
    Let $f(z) = z$ for $z\in x$.
\end{proof}