Cases_on record values should use <|-|> cases theorem

[mn200]

At the moment, this tactic reveals the underlying use of a constructor, one that should be generally hidden.