Entendídestruct ya que rompe una definición inductiva en sus constructores. Recientemente vicase_eq y no pude entender lo que hace de manera diferente?

1 subgoals
n : nat
k : nat
m : M.t nat
H : match M.find (elt:=nat) n m with
    | Some _ => true
    | None => false
    end = true
______________________________________(1/1)
cc n (M.add k k m) = true

En el contexto anterior, si destruyoM.find n m divide H en verdadero y falso mientras quecase_eq (M.find n m) deja H intacto y agrega una propuesta separadaM.find (elt:=nat) n m = Some v, que puedo reescribir para obtener el mismo efecto que destruct.

¿Puede alguien explicarme la diferencia entre las dos tácticas y cuándo se debe usar?