Tactics' agda-split can destroy matches

[isovector]

data ADT = One | Two Int | Three | Four Bool ADT | Five

case_split :: ADT -> Int
case_split One = _
case_split (Two i) = _
case_split Three = _
case_split (Four b a) = _  -- here
case_split Five = _

Splitting on either b or a at -- here deletes the entire case_split (Four b a) match.

[isovector]

:(