case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ (α → β) = (α → β')
α α' : Sort u
β β' : Sort v
h : α = α'
h' : α' → β = β'
⊢ (α → β) = (α' → β')
cases h
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ ((x : α) → (fun x => β) x) = (α → β')
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ (α → β) = (α → β')
show (∀ (x : α), (fun _ => β) x) = _
no goals
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ ((x : α) → (fun x => β) x) = (α → β')
rw [funext h']