SSReflect の case タクティックは，否定 (not, ~ A) に関しても場合分けしてくれる．

だが，その前に，普通のを見てみる．

  ============================
   forall b : bool, b -> G

という状況で，case. とすると，

2 subgoals, subgoal 1 (ID 10)
  
  G : Prop
  ============================
   true -> G

subgoal 2 (ID 11) is:
 false -> G

となる．そりゃそうだ．

inductive type を値の型とする関数も case ができるようだ．
実験してみるとなかなか不思議な仕様であるように思われる:

1 subgoals, subgoal 1 (ID 3)
  
  f : nat -> bool
  ============================
   f 3 && f 2 == f 1

この状況で， case f. とすると，

2 subgoals, subgoal 1 (ID 4)
  
  f : nat -> bool
  ============================
   true && f 2 == f 1

subgoal 2 (ID 5) is:
 false && f 2 == f 1

となる．うーむ．ま，それはそれとして，適用するものがないと，作れと要求される．

1 subgoals, subgoal 1 (ID 2)
  
  f : bool -> bool
  ============================
   nat

この状況で，case f. とすると，

3 subgoals, subgoal 1 (ID 3)
  
  f : bool -> bool
  ============================
   bool

subgoal 2 (ID 4) is:
 nat
subgoal 3 (ID 5) is:
 nat

となる．順に，場合分けに使うfの定義域の値の要求，値が true の場合と false の場合の
nat値の要求，となっている．実際，case f. の代わりに
case f; [exact true | exact 10 | exact 20]. とすると
定義ができて，Print してみると，

fun f : bool -> bool => if f true then 10 else 20
     : (bool -> bool) -> nat

となる．

やっと本題．こういうわけなので，

  ============================
   ~ A -> G

という状況で，case.すると，
~A は，関数 A -> False のことなので，
A のどの値で見るか，というのを尋ねる1個と，False の constructor の数 ( = 0 個) の
和の分だけの subgoal ができるわけで，

  ============================
   A

となる．