Why fail apply?

Signature File

sig lc.

kind tm,ty type.

type c tm.
type app tm -> tm -> tm.
type abs (tm -> tm) -> tm.

type top ty.
type arrow ty -> ty -> ty.

type ty ty -> o.
type of tm -> ty -> o.
type step tm -> tm -> o.

Module File

module lc.

ty top.
ty (arrow A B) :- ty A,ty B.
of (app M N) B :- of M (arrow A B), of N A.
of (abs R) (arrow A B) :- ty A,pi x\ (of x A => of (R x) B).

of c A :- ty A.

step (app M N) (app M' N ) :- step M M'.
step (app M N) (app M  N') :- step M N'.
step (app (abs R) M) (R M).
step (abs R) (abs R') :- pi x\ step (R x) (R' x).

I want to prove next Theorem

Welcome to Abella 1.3.4
Abella < Specification "lc".
Reading specification lc

Abella < Close tm,ty.

Abella < Define sn : tm -> prop by sn M := forall N,{step M N} -> sn N.

Abella < Theorem lamSN : forall F T,sn (F T) -> sn (abs F).


  ============================
   forall F T, sn (F T) -> sn (abs F)

lamSN < induction on 1.


  IH : forall F T, sn (F T) * -> sn (abs F)
  ============================
   forall F T, sn (F T) @ -> sn (abs F)

lamSN < intros.

  Variables: F, T
  IH : forall F T, sn (F T) * -> sn (abs F)
  H1 : sn (F T) @
  ============================
   sn (abs F)

lamSN < case H1.

  Variables: F, T
  IH : forall F T, sn (F T) * -> sn (abs F)
  H2 : forall N, {step (F T) N} -> sn N *
  ============================
   sn (abs F)

lamSN < unfold.

  Variables: F, T
  IH : forall F T, sn (F T) * -> sn (abs F)
  H2 : forall N, {step (F T) N} -> sn N *
  ============================
   forall N, {step (abs F) N} -> sn N

lamSN < intros.

  Variables: F, T, N
  IH : forall F T, sn (F T) * -> sn (abs F)
  H2 : forall N, {step (F T) N} -> sn N *
  H3 : {step (abs F) N}
  ============================
   sn N

lamSN < case H3.

  Variables: F, T, N, R'
  IH : forall F T, sn (F T) * -> sn (abs F)
  H2 : forall N, {step (F T) N} -> sn N *
  H4 : {step (F n1) (R' n1)}
  ============================
   sn (abs R')

lamSN < inst H4 with n1 = T.

  Variables: F, T, N, R'
  IH : forall F T, sn (F T) * -> sn (abs F)
  H2 : forall N, {step (F T) N} -> sn N *
  H4 : {step (F n1) (R' n1)}
  H5 : {step (F T) (R' T)}
  ============================
   sn (abs R')

lamSN < apply H2 to H5.

  Variables: F, T, N, R'
  IH : forall F T, sn (F T) * -> sn (abs F)
  H2 : forall N, {step (F T) N} -> sn N *
  H4 : {step (F n1) (R' n1)}
  H5 : {step (F T) (R' T)}
  H6 : sn (R' T) *
  ============================
   sn (abs R')

lamSN < apply IH to H6.
Error: Unify.UnifyError(0) %% Why??

  Variables: F, T, N, R'
  IH : forall F T, sn (F T) * -> sn (abs F)
  H2 : forall N, {step (F T) N} -> sn N *
  H4 : {step (F n1) (R' n1)}
  H5 : {step (F T) (R' T)}
  H6 : sn (R' T) *
  ============================
   sn (abs R')