Problem:
f(x) -> g(f(x))
g(f(x)) -> x
g(x) -> a()
Proof:
Containment Processor: loop length: 1
terms:
f(x)
context: g([])
substitution:
x -> x
Qed