I disagree. I think the key insight is to carry the proof with you in the structure of the type you 'parse' into.