The aim of this project is to formalize propositional logic with the later modality. This modality is used by the Iris framework (1) as a technique to prove properties of recursive programs (2), which is also called guarded recursion (3). We introduce a new axiom to prove completeness:
For all formulas P and Q, either P implies Q, or later Q implies P.
coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile