• Extensional Equality
• Why does Coq not have Extensional Equality?
• Comments by ThorstenAltenkirch