blob: 2a823396d504bee0152a76af4eb21d25cf2ae644 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
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'
|
