Hola:
Supongo que llegás a algo así:
⋮
—————–
y='c₀
——————————————————————————— I→
∀x f(x,y)='x → y='c₀
——————————————————————————— I∀
∀y (∀x f(x,y)='x → y='c₀)
La sugerencia es que uses RI₃ (transitividad). También necesitás algún RI₂ para acomodar bien las igualdades.
⋮ ⋮
y ='?? ?? ='c₀
—————–—————–—————– RI₃
y='c₀
——————————————————————————— I→
∀x f(x,y)='x → y='c₀
——————————————————————————— I∀
∀y (∀x f(x,y)='x → y='c₀)
Tenés que determinar cuál sería el termino ?? que se puede deducir de las hipótesis dadas y la hipótesis generada por la introducción del entonces.