induction p <;> aesop
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
no goals