从上下文中删除无用的假设

Question

有时我在证明上下文中有一个我已经使用过的假设，现在我知道我不再需要它了。为了在我进行证明时保持上下文整洁，我想删除这个假设。有什么策略可以做到这一点吗？

Answer 1

使用clear战术：

之前：

1 goal
  
  stuff ...
  H : T
  ============================
  goal

clear H.

之后：

1 goal
  
  stuff ...
  ============================
  goal

Answer 2

如果您使用 SSReflect 证明语言，您可以使用 {H} 符号清除假设 H。这可以在许多策略之后内联完成，例如 move 或 rewrite，如：

rewrite foo bar => {H}