> Extensionality fails in most dependent type theories

Is this a reason to use Isabelle?

I remember Bob Harper being interested in dependent typing. What is his take on extensionality?