The command has indeed failed with message:
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Tactic failure: Already an intensional equality.
The command has indeed failed with message:
Hypothesis e depends on the body of H'