421f2c2ae2
This commit fix a bug reported at comment https://github.com/leanprover/lean/issues/1827#issuecomment-368258713 Remark: the original problem reported at issue #1827 has nothing to do with this bug.
17 lines
486 B
Text
17 lines
486 B
Text
lemma subst_weirdness1 {α β : Type} {x : α} {P : Π t : Type, t → Prop}
|
||
(H : β = α)
|
||
(H' : P α x)
|
||
: P β (cast (by cc) x) :=
|
||
by { subst β, exact H' }
|
||
|
||
lemma subst_weirdness2 {α β : Type} {x : α} {P : Π t : Type, t → Prop}
|
||
(H : β = α)
|
||
(H' : P α x)
|
||
: P β (cast (by cc) x) :=
|
||
by { cases H, exact H' }
|
||
|
||
lemma subst_weirdness {α β : Type} {x : α} {P : Π t : Type, t → Prop}
|
||
(H : β = α)
|
||
(H' : P α x)
|
||
: P β (cast (by cc) x) :=
|
||
by { subst α, exact H' }
|