Weich's IPC in SSReflect

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"