Problem: f(g(x),x) -> f(a(),x) f(h(x),y) -> f(h(x),h(x)) g(x) -> p(x) p(x) -> a() Proof: Open