proving boolean equality

Stream: lean4

[David Renshaw]

How do I prove a boolean equality such as

example (y : Nat) : y == y :=
  by admit

?

[Mario Carneiro]

there should be an eq_of_beq theorem

[Mario Carneiro]

Nat.eqOfBeqEqTrue exists but goes in the wrong direction (x == y -> x = y). You can derive it from Nat.neOfBeqEqFalse though

[David Renshaw]

Thanks. Looks like my problems also go away if I just switch to using propositional equality.