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

State before:
V : Type u_1
inst✝ : SetTheory V
β α✝ : Type
a✝ : Nat
p : BoundedFormula α✝ a✝
vα : α✝ → V
vβ : β → V
l : Fin a✝ → V
⊢ Interpret V (sum β p) (Sum.elim vα vβ) l ↔ Interpret V p vα l
Tactic:
induction p <;> aesop
State after:
no goals