Library mcertikos.proc.IPCIntroGen
This file provide the contextual refinement proof between PKContextNew layer and PThreadIntro layer
Require Export IPCIntroGenDef.
Require Export IPCIntroGenFresh.
Require Export IPCIntroGenPassthrough.
Require Export IPCIntroGenFresh.
Require Export IPCIntroGenPassthrough.