The token-level round trip, by induction over the expression
theorem M_all (c : Ctx) : ∀ n e, sizeOf e < n → isE e = true → M c e
Every well-formed expression carries the round-trip facts.
def parseToks (sf : Sf) (S : Sym) (ts : List Tok) : Option Json
Read a whole token list as one expression.
theorem parseToks_print (sf : Sf) (S : Sym) (e : Json) (he : isE e = true) :
parseToks sf S (print sf S e) = some e
The token-level round trip: every well-formed expression reads back from its printed tokens, on both surfaces and under every symbol table.