Bugs found in the kernel as a result of formalization https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Soundness.20bug.3A.20hasLooseBVars.20is.20not.20conservative/near/521286338 leanprover/lean4#10475 leanprover/lean4#10511