Merged requested to merge robbert/sprop into master
Following the discussions on Iris-club, hereby a merge request for
siProp. I created this file already a long time ago, but never did do anything with it.
- Defines the type
siPropof step-indexed propositions
- Defines the operators of an intuitionistic logic + equality + later.
- Proves the basic laws of these operators.
- Proves soundness statements.
- Shows that
siPropforms an SBI so we get support in the proofmode.