Skip to content

Formulate `is_closed_expr` in terms of `gset`s.

Dan Frumin requested to merge dfrumin/iris-coq:is_closed_gset into master

..And prove some additional lemmas.

Following a discussion w/ @robbertkrebbers

Since it is not necessary for is_closed_expr to simplify well, it might be better to formulate it in terms of sets, not lists. This is convenient when you have e.g. a description of a type system where contexts are maps, and you want to prove that all well-typed expressions are appropriately closed.

Merge request reports