Lean Kernel Arena / bugs/nat-rec-k-lie

Proof of False via trusted k on Nat.rec.

Lie by claiming Nat.rec is K-like. Then replace the major premise by Nat.zero, but nat literals bypasses K-like reduction, so two reduction rules disagree.

∀ n, g n holds by the first, and g 1 is False by the second.

A variant of bugs/rec-k-lie, which nanoda and its descendants accepted until it was fixed; at that time, nanoda itself rejected this variant, as it had no literal path for Nat.rec.