Added proof of isok_Ok.
Merged.