[
  {"type":"KeywordNamespace","value":"def"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"f"},
  {"type":"Operator","value":"("},
  {"type":"Name","value":"x"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Nat"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Nat"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"NameBuiltinPseudo","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"x"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"+"},
  {"type":"TextWhitespace","value":" "},
  {"type":"LiteralNumberInteger","value":"1"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentSingle","value":"-- comment"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"KeywordNamespace","value":"theorem"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"thm"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"q"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"r"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordType","value":"Prop"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∧"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Name","value":"q"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∨"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"r"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"→"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∧"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"q"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∨"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∧"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"r"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"NameBuiltinPseudo","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Keyword","value":"by"},
  {"type":"TextWhitespace","value":"\n  "},
  {"type":"Name","value":"intro"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"⟨"},
  {"type":"Name","value":"hp"},
  {"type":"Operator","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hqr"},
  {"type":"NameBuiltinPseudo","value":"⟩"},
  {"type":"TextWhitespace","value":"\n  "},
  {"type":"Keyword","value":"show"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∧"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"q"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∨"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"("},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∧"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"r"},
  {"type":"Operator","value":")"},
  {"type":"TextWhitespace","value":"\n  "},
  {"type":"Name","value":"cases"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hqr"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Keyword","value":"with"},
  {"type":"TextWhitespace","value":"\n  "},
  {"type":"NameBuiltinPseudo","value":"|"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"inl"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hq"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"=\u003e"},
  {"type":"TextWhitespace","value":"\n    "},
  {"type":"Keyword","value":"have"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hpq"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∧"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"q"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"NameBuiltinPseudo","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"And"},
  {"type":"NameBuiltinPseudo","value":"."},
  {"type":"Name","value":"intro"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hp"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hq"},
  {"type":"TextWhitespace","value":"\n    "},
  {"type":"Name","value":"apply"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Or"},
  {"type":"NameBuiltinPseudo","value":"."},
  {"type":"Name","value":"inl"},
  {"type":"TextWhitespace","value":"\n    "},
  {"type":"Name","value":"exact"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hpq"},
  {"type":"TextWhitespace","value":"\n  "},
  {"type":"NameBuiltinPseudo","value":"|"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"inr"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hr"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"=\u003e"},
  {"type":"TextWhitespace","value":"\n    "},
  {"type":"Keyword","value":"have"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hpr"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"p"},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltinPseudo","value":"∧"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"r"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":":"},
  {"type":"NameBuiltinPseudo","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"And"},
  {"type":"NameBuiltinPseudo","value":"."},
  {"type":"Name","value":"intro"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hp"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hr"},
  {"type":"TextWhitespace","value":"\n    "},
  {"type":"Name","value":"apply"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Or"},
  {"type":"NameBuiltinPseudo","value":"."},
  {"type":"Name","value":"inr"},
  {"type":"TextWhitespace","value":"\n    "},
  {"type":"Name","value":"exact"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"hpr"},
  {"type":"TextWhitespace","value":"\n"}
]