@user21820 Yup, I have proved it already yesterday, the only goal worth mentioning was proving the uniqueness of h as a function, that is to prove that forall x in N forall y1,y2 in A if (x,y1) in h and (x,y2) in h then y1 = y2. Here, we take an induction on x and then use an alternative induction principle: if b subset h and (0,a) in b and forall s,t (s,t) in b -> (S(s), F(t)) in b then b = h
So, for example to prove that if (0,y1) in h and (0,y2) in h then y1 = y2
We prove that both are equal to a.