Module `iris.algebra.big_op` exports unqualified `foo`
Minor issue — iris.algebra.big_op
uses foo
for the name of an instance. A more unique name might be better.
From iris.program_logic Require Import ectx_lifting.
About foo.
foo : ∀ (A : Type) (R : relation A), RewriteRelation R
Argument A is implicit and maximally inserted
Argument scopes are [type_scope _]
foo is transparent
Expands to: Constant iris.algebra.big_op.foo