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

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

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