Following the discussions on Iris-club, hereby a merge request for
sProp. I created this file already a long time ago, but never did do anything with it.
- Defines the type
sPropof step-indexed propositions
- Defines the operators of an intuitionistic logic + equality + later.
- Proves the basic laws of these operators.
- Proves soundness statements.
sPropforms an SBI so we get support in the proofmode.