1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
File "./output/FunExt.v", line 15, characters 5-24:
The command has indeed failed with message:
Tactic failure: Not an extensional equality.
File "./output/FunExt.v", line 17, characters 5-24:
The command has indeed failed with message:
Tactic failure: Not an extensional equality.
File "./output/FunExt.v", line 18, characters 5-26:
The command has indeed failed with message:
Tactic failure: Not an extensional equality.
File "./output/FunExt.v", line 93, characters 9-28:
The command has indeed failed with message:
Tactic failure: Not an extensional equality.
File "./output/FunExt.v", line 149, characters 9-28:
The command has indeed failed with message:
Tactic failure: Already an intensional equality.
File "./output/FunExt.v", line 162, characters 9-29:
The command has indeed failed with message:
Hypothesis e depends on the body of H'
|
