Lean's treatment of type equalities

Stream: lean4

[Arnav Sabharwal]

How does Lean handle terms of type 1 in the context of a proof that type 1 = type 2? Here is an MWE providing a specific instance of my question (a bit contrived):

theorem MWE : Bool.true = Bool.false := by {
  let dummy := fun (x : Nat) => Bool.true
  -- this is a dummy type equality, but one can expect genuine ones
  let test_equality : Nat = Bool := by sorry
  let c := dummy Nat.zero
  rw [← test_equality] at dummy
  -- why does the infoviewer shadow dummy?
  -- why is c : Nat not displayed?
}

This seems to be a fundamental misunderstanding on my end, so a clarification would really help! Thanks!

[Kyle Miller]

When you rewrite a hypothesis, the way it works is it creates a new local hypothosis and (tries to) delete the old one. Since dummy is used in c, it can't delete dummy, so you get two copies, the new one shadowing the old one.