Currently the logic here
https://github.com/theindigamer/ats2-mode/blob/d08ac0287a5ac7161a856520dcddb6a012f07d23/ats2-mode.el#L180-L190
means that when you have a situation like
the region case foo of | will get highlighted using the wrong face which doesn't make sense. The highlighting should only apply to proofs.
Currently the logic here
https://github.com/theindigamer/ats2-mode/blob/d08ac0287a5ac7161a856520dcddb6a012f07d23/ats2-mode.el#L180-L190
means that when you have a situation like
the region
case foo of |will get highlighted using the wrong face which doesn't make sense. The highlighting should only apply to proofs.