blob: 4a83375f6fbb43b50b3e4ccc9b15f187796bedb4 (
plain)
1
2
3
4
|
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.].
|
