cases p <;> rfl
V : Type u_3
inst✝ : SetTheory V
α : Type u_1
n : Nat
vα : α → V
β✝ : Type u_2
vβ : β✝ → V
l : Fin n → V
p : α ⊕ Fin n
⊢ interpretTerm V (Sum.elim vα vβ) l (termSum p) = interpretTerm V vα l p
no goals