Where's the equation lemma for `not`?

Stream: general

[Eric Wieser]

Why does src#not have no equation lemmas, but my identical definition below does?

def not2 (a : Prop) := a → false

-- not2.equations._eqn_1 : ∀ (a : Prop), not2 a = (a → false)
#check not2.equations._eqn_1

-- doesn't exist
#check not.equations._eqn_1

[Mario Carneiro]

Because not is defined before eq