Skip to content
GitLab
Explore
Sign in
Lennard Gäher
Iris
Repository
iris
theories
heap_lang
proph_erasure.v
Find file
Blame
History
Permalink
Rename lemma `not_stuck_under_ectx` → `not_stuck_fill`, to be consistent with `stuck_fill`.
· 8e455e52
Robbert Krebbers
authored
Nov 25, 2019
Also refactor the proofs to make better reuse of existing lemmas.
8e455e52