Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).