On Partial functions (Solution)
The answer is
NO !!!!
.
The axiom
pfun_extensionality
allows you to prove 0=1 (look at
this file
).
If you remove this axiom, the formalization is OK.
Going home