> My intuition is: evaluating in Lean and embedding the result in the toy language is identical to big step evaluation in the toy language.
Yes, I think that's right.
> But I can't parse the theorem.
I think there's a bit of a divide between languages with tactic-based proofs and languages without tactics, and it looks like both Lean and Isabelle use tactics.
I've gotten very comfortable with Agda over the past year. Agda doesn't have a real tactics metalanguage; but I honestly prefer working with proof terms, since it's easier (I feel) to write comprehensible proofs. While tactics make for very compact proofs, I think giving a proof some space to breathe is a good thing -- I'm interested in why it's true, not only that it's true.
I think the analogous theorem in Conor McBride's Agda version of this development is here [1]:
ev=>* : {t : Ty} (x : Exp t)
-> x =>* ve (ev x)
where "eval _" in Lean becomes "ev x", and "_.embed" becomes "ve _".
The theorem body is heavily commented (nice!), and each case is handled explicitly and in full. While the development is probably a little bit longer than in Lean or Isabelle, I find it easier to approach.
[1] https://github.com/pigworker/Samizdat/blob/main/ExampleSeman...
> I could not write this stuff. It looks simple but it isn't.
True that. I bounced a number of times off of proof assistants before it stuck. Like I said, I feel very comfortable with Agda now; but I won't claim this is easy.