clear

clear

不要な前提を消去するタクティック。不要な前提が多すぎてごちゃごちゃしすぎる場合に見た目をすっきりさせることができる。ただし不要じゃない前提を消してしまった場合は証明できなくなってしまうので注意。

1 subgoal
  
  P : Prop
  Q : Prop
  H : P
  H0 : Q
  ============================
   P

Unnamed_thm < clear H0.
1 subgoal
  
  P : Prop
  Q : Prop
  H : P
  ============================
   P