Clarify trust requirements on kernel

Author: OrfeasLitos

Manual/Elaboration.lean

@@ -99,7 +99,8 @@ Roughly speaking, Lean's processing of a source file can be divided into the fol
 
 : Kernel Checking
 
-  Lean's trusted kernel checks the output of the elaborator to ensure that it follows the rules of the type theory.
+  Lean's trusted kernel{margin}[To avoid trusting the elaborator when verifying a statement, one has to {keywordOf Lean.Parser.Command.print}`#print` the statement to get the elaborated type and manually verify that it expresses the desired statement.
+  This brings {keywordOf Lean.Parser.Command.print}`#print` into the trusted base.] checks the output of the elaborator to ensure that it follows the rules of the type theory.
 
 : Compilation