diff --git a/tests/lean/run/cases_bug.lean b/tests/lean/run/cases_bug.lean index 706df951a8..76f4f91c64 100644 --- a/tests/lean/run/cases_bug.lean +++ b/tests/lean/run/cases_bug.lean @@ -1,4 +1,4 @@ import logic.cast -theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a +theorem cast_heq₂ : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a | A A (eq.refl A) a := heq_of_eq !cast_eq