I'm guessing this is the reason that stripping is not working in my proof (see attached). It looks trivial but I can't see a way to finish it without getting stuck into the HOL embedding. (As shown, renaming the schema components partially helps.) Can anyone think of a Z work-around for now?
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com