Skip to content

Add `head_prim_fill_reducible`.

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

A more general implication from head_reducible to reducible.

Merge request reports