es11



 b:t1->t2,c:t1, y:t2 |- c:t1      b:t1->t2,c:t1 |- b:t1->t2   b: t1->t2, c: t1 |- c: t1
------------------------------    -------------------------------------------------------
b:t1->t2, c:t1 |- \y.c:t2->t1                b: t1->t2, c: t1 |- (bc): t2
---------------------------------------------------------------------------
            b:t1->t2, c:t1 |- (\y.c)(bc): t1
         ---------------------------------------
            b:t1->t2 |- \c.((\y.c)(bc)): t1->t1
          ---------------------------------------------
            |- \bc.((\y.c)(bc)): (t1->t2)->t1->t1