Parciales

Hola. Estaba haciendo este ejercicio pero me surgio una duda en la parte b.

Primero planteé el ERP para POSF como sigue:

Sea A el alfabeto definido en la parte a y PROP' el conjunto inductivo definido en la parte a, y sean:

$\displaystyle {{f}_{0}}\in PROP'$

$\displaystyle {{f}_{1}}\in PROP'$

$\displaystyle {{f}_{2}}:A\times POSF\times PROP'\to PROP'$

$\displaystyle {{f}_{3}}:A\times POSF\times POSF\times PROP'\times PROP'\to PROP'$

Entonces existe una única funcion $\displaystyle f:POSF\to PROP'$ tal que:

$\displaystyle f\left( {{p}_{0}} \right):={{p}_{0}}={{f}_{0}}$

$\displaystyle f\left( {{p}_{1}} \right):={{p}_{1}}={{f}_{1}}$

$\displaystyle f\left( \varphi \neg \right):=\left( \neg f\left( \varphi \right) \right)={{f}_{2}}\left( x,\varphi ,f\left( \varphi \right) \right)$

$\displaystyle f\left( \varphi \psi \to \right):=\left( f\left( \varphi \right)\to f\left( \psi \right) \right)={{f}_{3}}\left( x,\varphi ,\psi ,f\left( \varphi \right),f\left( \psi \right) \right)$

Ahora, ¿como pruebo que es invertible (antes de definir la que viene)? Veo que hay una correspondencia uno a uno pero formalmente como deberia mostrarlo? Gracias