A port of https://github.com/coq-contribs/ipc to SSReflect.
Reuses parts of FCSL-PCM, FAV and compact data structures.
References:
- Weich, [1998] "Decision procedures for intuitionistic propositional logic by program extraction"
- Weich, [2001] "Improving proof search in intuitionistic propositional logic"