/* Exported from KeYmaera X v4.9.8 */

Theorem "Tactic editor only lets me edit first branch".

Definitions
Real x0 = (1);
Real v0 = (2);
Real a = (3);
End.

ProgramVariables
Real x;
Real v;
End.

Problem
  x = x0 & v = v0 -> [{x'=v,v'=a}] x >= x0
End.

Tactic "Tactic editor only lets me edit first branch"
implyR('R=="x=x0()&v=v0()->[{x'=v,v'=a()}]x>=x0()");
dC("v>=v0()", 'R=="[{x'=v,v'=a()}]x>=x0()"); <(
  expandAll;
  todo,
  todo
)
End.

End.