Skip to content

Add `head_prim_fill_reducible`.

Dan Fruminrequested to merge
dfrumin/iris-coq:head_prim_fill_reducible into master

A more general implication from head_reducible to reducible.

Merge request reports