Maybe it is worth emphasizing that Proof is not a built-in type

[zxch3n]

https://github.com/leanprover/theorem_proving_in_lean4/blob/ee6aeb4f1db92c3fed2121944bdd1d4871d6d851/propositions_and_proofs.md?plain=1#L36-L38

It has brought some confusion https://stackoverflow.com/questions/69182724/lean-4-unknown-identifier-proof . People may also try the code on their editor.

[pimotte]

Same holds for Implies, which I ran into. I do get the educational lie, it reads nicely this way. I don't really see how to communicate this properly without interrupting the flow of text.