The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/12/2016 06:52 PM, Thorsten Altenkirch wrote:
> Yes, indeed. Functions without extensionality are like bread without butter. 
> :-)
>
> Thorsten

All that is really needed is a very weak form of functional 
extensionality, applying only to functions from negated equalities to False:

Axiom neq_False_extensionality : forall A (a b :A)(f g : (a<>b) -> 
False), (forall p:(a<>b), f p = g p) -> f = g.

By operating only on Prop functions, this seems to avoid at least one 
criticism of functional extensionality in Coq - that it can interfere 
with the preservation of properties like complexity between extracted 
code and the original Coq source.

-- Jonathan