## Summary Port [`program_logic/total_ectx_lifting.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/program_logic/total_ectx_lifting.v). ## Dependencies **Rocq dependencies:** - `proofmode/proofmode` (aggregation) - #344 - #347 - #350
Summary
Port
program_logic/total_ectx_lifting.v.Dependencies
Rocq dependencies:
proofmode/proofmode(aggregation)