feat: Big separating conjunction (PR B)#2

Open

hxrts wants to merge 7 commits intomasterfrom

fork/iris/big-op

Commits on Jan 29, 2026

Add FiniteMap interface

lzy0505
authored and
hxrts
committed
Clean up list lemmas

lzy0505
authored and
hxrts
committed
Add code

lzy0505
authored and
hxrts
committed
Clean up BigOpL

lzy0505
authored and
hxrts
committed
Fix build

lzy0505
authored and
hxrts
committed
Clean up BigOpM

lzy0505
authored and
hxrts
committed
feat: Add BI-level big separating conjunction
hxrts
committed