Theorem: SetTheory.interpret_termSum_elim (SetTheory/Formula.lean)

State before:
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
Tactic:
cases p <;> rfl
State after:
no goals