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

[zxch3n]

theorem_proving_in_lean4/propositions_and_proofs.md

Lines 36 to 38 in ee6aeb4

	We could then introduce, for each element ``p : Prop``, another type
	``Proof p``, for the type of proofs of ``p``. An "axiom" would be a
	constant of such a type.

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.