create iris_meta file for meta-theorems (adequacy, lifting lemmas). formulate two of our four lifting lemmas.