chore(data/subtype): add heq_of_coe_eq ext lemma

[eric-wieser]

This means that ext breaks equality of sigma types into the following goals:

example {ι : Sort*} {α : Type*} {p : ι → α → Prop} {a b : Σ i, subtype (p i)} : a = b :=
begin
  ext,
  sorry, -- a.fst = b.fst
  sorry, -- p a.fst x ↔ p b.fst x
  sorry, -- ↑(a.snd) = ↑(b.snd)
end

---

This overlaps with #6257, although we probably want both lemmas.

[eric-wieser]

This fails, but I don't understand why.

[bryangingechen]

Replacing the ext1 before the failing change with show_term { ext1 } before this PR returns:

Try this: refine subtype.ext _

And the goal becomes: ↑(bitvec.of_nat n (bitvec.to_nat ⟨xs, h⟩)) = ↑⟨xs, h⟩ where the coes are to list bool.

With this PR, it returns:

Try this: refine vector.ext (λ (m : fin n), _[m])

(For some reason, the suggestion has a stray [m] at the end; refine vector.ext (λ (m : fin n), _) results in the goal vector.nth (bitvec.of_nat n (bitvec.to_nat ⟨xs, h⟩)) m = vector.nth ⟨xs, h⟩ m as stated in the build error.)

I'm not sure why your change would have had this effect (but admittedly I don't know how ext1 works either).