There is a need to start porting `iris_heap_lang/derived_laws.v`, specifically the arrays part of it. In particular, it is required by: - porting of `wp_*` tactics (#480) - porting of Iris tutorial (https://github.com/logsem/iris-tutorial-lean) I'd like to claim the arrays.
There is a need to start porting
iris_heap_lang/derived_laws.v, specifically the arrays part of it. In particular, it is required by:wp_*tactics (Port HeapLang tactics #480)I'd like to claim the arrays.