Problem:
 app(app(const(),x),y) -> x
 app(app(app(subst(),f),g),x) -> app(app(f,x),app(g,x))
 app(app(fix(),f),x) -> app(app(f,app(fix(),f)),x)

Proof:
 Uncurry Processor:
  const2(x,y) -> x
  subst3(f,g,x) -> app(app(f,x),app(g,x))
  fix2(f,x) -> app(app(f,fix1(f)),x)
  app(const1(x5),x6) -> const2(x5,x6)
  app(const(),x6) -> const1(x6)
  app(subst2(x5,x4),x6) -> subst3(x5,x4,x6)
  app(subst1(x5),x6) -> subst2(x5,x6)
  app(subst(),x6) -> subst1(x6)
  app(fix1(x5),x6) -> fix2(x5,x6)
  app(fix(),x6) -> fix1(x6)
  Unfolding Processor:
   loop length: 5
   terms:
    fix2(subst1(x85456),x86194)
    app(app(subst1(x85456),fix1(subst1(x85456))),x86194)
    app(subst2(x85456,fix1(subst1(x85456))),x86194)
    subst3(x85456,fix1(subst1(x85456)),x86194)
    app(app(x85456,x86194),app(fix1(subst1(x85456)),x86194))
   context: app(app(x85456,x86194),[])
   substitution:
    x85456 -> x85456
    x86194 -> x86194
   Qed