FunExt.out

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'