debug.skipKernelTC を有効にすると、カーネルによる型検査が行われなくなります。結果として、不正な証明を Lean に受け入れさせることができてしまいます。