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

State before:
α : Sort u_1
γ : Sort u_2
x x' : α
β : α → Sort u_3
f : (x : α) → β x → γ
h : x = x'
y : β x
⊢ f x' (h ▸ y) = f x y
Tactic:
cases h
State after:
case refl
α : Sort u_1
γ : Sort u_2
x : α
β : α → Sort u_3
f : (x : α) → β x → γ
y : β x
⊢ f x (⋯ ▸ y) = f x y

State before:
case refl
α : Sort u_1
γ : Sort u_2
x : α
β : α → Sort u_3
f : (x : α) → β x → γ
y : β x
⊢ f x (⋯ ▸ y) = f x y
Tactic:
rfl
State after:
no goals