In krml178 page 40 the semantics of orders are specified. It would be nice to include that
const a extends b;
is equivalent to a != b && a <: b && ∀x. ((a==x || b==x) <==> ( a<:x && x<:b))
As <: is reflexive, I did not expect the a != b part to be valid.