Closed olaure01 closed 3 years ago
The auto-prover generates an error message on pre-prod !A ⊢ ?!?A.
Thanks @olaure01 ! I forgot to handle promotion properly : we cannot commute weakening if the weakening is on promoted formula.
The auto-prover generates an error message on pre-prod !A ⊢ ?!?A.