case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36468
c : γ
x : α ⊕ β
⊢ Sum.elim (const α c) (const β c) x = const (α ⊕ β) c x
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36468
c : γ
⊢ Sum.elim (const α c) (const β c) = const (α ⊕ β) c
ext x
no goals
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36468
c : γ
x : α ⊕ β
⊢ Sum.elim (const α c) (const β c) x = const (α ⊕ β) c x
cases x <;> rfl