-
Magnus Myreen authored
The problem was that the following tactic fs [Once validintervalboundscmd_side_def] applied the rewrite once in the goal and once in the assumptions. It is safer to use simp [Once ...] or once_rewrite_tac [...].
57aed088
The problem was that the following tactic fs [Once validintervalboundscmd_side_def] applied the rewrite once in the goal and once in the assumptions. It is safer to use simp [Once ...] or once_rewrite_tac [...].