bug with refine + rw

Stream: general

[Kenny Lau]

example (H : (0 = 0 → 0 = 1) → true) : true :=
begin
  refine H (λ h, _), rw h --fails
/-
rewrite tactic failed, lemma is not an equality nor a iff
state:
H : (0 = 0 → 0 = 1) → true,
h : 0 = 0
⊢ 0 = 1
-/
end


example (H : (0 = 0 → 0 = 1) → true) : true :=
begin
  refine H _, intro h, rw h --works
end

[Kenny Lau]

and also workaround:

example (H : (0 = 0 → 0 = 1) → true) : true :=
begin
  refine H (λ h, _),
  change _ at h, rw h --works
end