Skip to content
GitLab
Explore
Sign in
Iris
Iris
Issues
#143
Gen_proofmode: move internal eq into SBI
If the Bi is not step-indexed, then there is no reason not to use the pure embedding.