The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Already an intensional equality.
The command has indeed failed with message:
In nested Ltac calls to "extensionality in (var)" and
"clearbody (ne_var_list)", last call failed.
Hypothesis e depends on the body of H'