[caotic123]

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

[caotic123]

As far i know, pompom has a decidable type check though.