L : Language
L' : Language
M : Type w
N : Type ?u.56171
P : Type ?u.56174
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
⊢ Realize (∼φ ⟹ ψ) v xs ↔ Realize φ v xs ∨ Realize ψ v xs
L : Language
L' : Language
M : Type w
N : Type ?u.56171
P : Type ?u.56174
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
⊢ Realize (φ ⊔ ψ) v xs ↔ Realize φ v xs ∨ Realize ψ v xs
simp only [realize, Sup.sup, realize_not, eq_iff_iff]
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.56171
P : Type ?u.56174
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
⊢ Realize (∼φ ⟹ ψ) v xs ↔ Realize φ v xs ∨ Realize ψ v xs
tauto