Skip to content

Let `iExFalso` perform `iStartProof`.

Robbert Krebbers requested to merge robbert/iExFalso_iStartProof into master

Before you would get some internal error message that apply tac_ex_falso failed because the goal is not env_entails.

Merge request reports