Provide smart `bi` constructor for BIs that are not step-indexed
In that case, we can just define the distance relation on the OFE as:
P ≡{n}≡ Q := P ⊢ Q ∧ Q ⊢ P
And all Proper
axioms should be admissible.
In that case, we can just define the distance relation on the OFE as:
P ≡{n}≡ Q := P ⊢ Q ∧ Q ⊢ P
And all Proper
axioms should be admissible.