Re: Predicate subtypes

[Marieke Huisman <Marieke.Huisman@sophia.inria.fr>]

Hello Pertti,

I think you have a problem with the K_conversion.

If you make a lemma
  lem : LEMMA
    f1

and you try to prove it, by expanding f1 you get the following goal:
lem :  

  |-------
{1}   FORALL (now, next: st, cc: c):
        p(cc, next) AND px(cc, now) = K_conversion(0)

Your px function has type [c, st -> [st -> int]] (with the 
restriction that the first two arguments have to satisfy p), and thus 
you don't give enough arguments.

Best regards,

Marieke Huisman