Comment by BalinKing

I also took a look at the `LangRust.lean`, and the majority of the proofs are just `rfl` (after an `intros`)—that's a major red flag, since it means the "theorems", like those in SSOT.lean, are true just by unfolding definitions. In general, that's basically never true of any interesting fact in programming languages (or math in general); on the contrary, it takes a lot of tedious work even to prove simple things in Lean.