Theorem: heq_dcast_left (Extra/Cast/DCast.lean)

State before:
α : Sort u_1
a b c : α
motive : α → Sort u_2
h : a = b
t : motive a
u : motive c
⊢ HEq (dcast h t) u ↔ HEq t u
Tactic:
cases h
State after:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
u : motive c
⊢ HEq (dcast ⋯ t) u ↔ HEq t u

State before:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
u : motive c
⊢ HEq (dcast ⋯ t) u ↔ HEq t u
Tactic:
rfl
State after:
no goals