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

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

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

===============================
Input Problem:
===============================
Gamma ={
  A1[(app (\ X1.S3) R1)] =?= (app (\ X2.S4) T1[(letrec {E6;E7} in S5)])}
Delta1=  {}
Delta2=  {}
Delta3=  {}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (app (\ X2.S4) T1[(letrec {E6;E7} in S5)])
  =?=
  (app (\ X2.S4) T1[(letrec {E6;E7} in S5)])
Sol = {
  A1 |-> [.],
  R1 |-> T1[(letrec {E6;E7} in S5)],
  X1 |-> X2,
  S3 |-> S4}
Delta1  = 
  {}
Delta2 = 
  {}
Delta3 = 
  {}