Schedule/ProofCafe_20

remember

  • remember T. destruct t. はcase_eq T. と似ている。
  • destruct (式). の式の部分が変数一つならばrememberやcase_eqは必要ない。
  • そもそもboolを使わずsumboolを使っていればよい。

apply with

  • apply … with … は使う補題(定理)の引数が多いときなど有用。
  • ↑引数名がないときはどうする?
  • eapplyを使うという方法もある。