Let rel = ( type S , type T -> func([S,T],bool) ).
Given A in type and F in func(A,A) and c in A:
Let G = ( rel(nat,A) R -> R(0,c) and forall k in nat ( forall x in A ( R(k,x) implies R(k+1,F(x)) ) ) ).
Let S = ( nat k , A x -> forall R in rel(nat,A) ( G(R) implies R(k,x) ) ). // intersection of all relations satisfying G
Let Q = ( nat k -> forall x,y in A ( S(k,x) and S(k,y) implies x=y ) ). // uniqueness of mappings of k in S
// Proof that S satisfies G //
Given R in rel(nat,A) such that G(R):