corrected wrong showing of expressions, and lack of left-associativity
of <> in Def