[B]1   [A]2
      ------ →I(1)
       B → A
     ----------- →I(2)
      A → (B → A)                A
   --------------------------- →E
               B → A                B
             -------------------------- →E
                   A
Il lambda-termine corrispondente e' (λz.λt.z)xy, la cui forma normale e' x.