[PVS-Help] Unrecognized equality

[Jerome <jerome@xxxxxxxxxxxxxx>]

Does anyone know why the following doesn't produce Q.E.D in PVS?

  {-1}  strict_subset?(K!1, J!1) IMPLIES
	  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
  [-2]  strict_subset?(K!1, J!1)
    |-------
  [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))

  Rerunning step: (ASSERT)
  Simplifying, rewriting, and recording with decision procedures,
  this simplifies to:
  composable :

  {-1}  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
  [-2]  strict_subset?(K!1, J!1)
    |-------
  [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))

After I make ASSERT call I would think the proof was finished... am I
missing something? Thanks

jerome