=========================================================
Recognized function symbols in input:

  name                arity   strict-pos  binder-arity        
  ----                -----   -----       -----               
  \                   1       []          [1]                 
  app                 2       [1]         [0,0]               

=========================================================

===============================
Input Problem:
===============================
Gamma ={
  A2[(\ X3.S6)] =?= (app (\ X4.S7) (\ x5.(var x5)))}
Delta1=  {}
Delta2=  {}
Delta3=  {((var x5),(_internal_f [.]))}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (app (\ X4.S7) (\ x5.(var x5))) =?= (app (\ X4.S7) (\ x5.(var x5)))
Sol = {
  A2 |-> (app [.] (\ x5.(var x5))),
  A_#1 |-> [.],
  X3 |-> X4,
  S6 |-> S7}
Delta1  = 
  {A2}
Delta2 = 
  {}
Delta3 = 
  {((var x5),(_internal_f [.]))}