Errata to "An Intuitionistic Logic That Proves Markov's Principle", H. Herbelin
-------------------------------------------------------------------------------
(April 2021)
Typos
-----
On Figure 2, "/\^_E^o" should be "/\^_E^i", and "pi_1 p" should be "pi_i p".
Arguments of case, dest, efq were wrongly typeset in tt font.
Page 4, bottom of column 1:
- "catch_alpha only applies to proofs of forall-implication-formulas" should be
"catch_alpha only applies to proofs of forall-implication-free formulas",
- "one is sure that alpha does occur in V" should be
"one is sure that alpha does _not_ occur in V".
Thanks to Vincent Semaria for reporting.