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

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.or p q) v l ↔ Interpret V p v l ∨ Interpret V q v l
Tactic:
rw [or_iff]
State after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.or p q) v l ↔ ¬Interpret V p v l → Interpret V q v l

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.or p q) v l ↔ ¬Interpret V p v l → Interpret V q v l
Tactic:
rfl
State after:
no goals