The command has indeed failed with message:
Tactic failure: To use dependent destruction, first [Require Import Coq.Program.Equality.].
The command has indeed failed with message:
Tactic failure: To use dependent induction, first [Require Import Coq.Program.Equality.].