Me encuentro en la situación de que aplique el case de por ejemplo (a:bool)
Y de momento se me divide en 2, yo lo veo como un or (a=true \/ a=false) pero el problema que tengo es que una vez uso el case me sustituye las ocurrencias de a por True en una rama y por False en la otra. Bárbaro.
Pero si por alguna razón tengo ese a nuevamente, no tengo ninguna hipótesis que me permita rewrite el a por su valor del caso
Mi workaround:
cut (a=true \/ a=false); [intro|case a ; tauto].
elim H; intros.