case nil
L : Language
L' : Language
M : Type w
N : Type ?u.66568
P : Type ?u.66571
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
v : α → M
xs : Fin n → M
⊢ Realize (List.foldr (fun x x_1 => x ⊔ x_1) ⊥ []) v xs ↔ ∃ φ, φ ∈ [] ∧ Realize φ v xs

case cons
L : Language
L' : Language
M : Type w
N : Type ?u.66568
P : Type ?u.66571
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
v : α → M
xs : Fin n → M
φ : BoundedFormula L α n
l : List (BoundedFormula L α n)
ih : Realize (List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l) v xs ↔ ∃ φ, φ ∈ l ∧ Realize φ v xs
⊢ Realize (List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (φ :: l)) v xs ↔ ∃ φ_1, φ_1 ∈ φ :: l ∧ Realize φ_1 v xs
L : Language
L' : Language
M : Type w
N : Type ?u.66568
P : Type ?u.66571
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
l : List (BoundedFormula L α n)
v : α → M
xs : Fin n → M
⊢ Realize (List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l) v xs ↔ ∃ φ, φ ∈ l ∧ Realize φ v xs
induction' l with φ l ih
no goals
case nil
L : Language
L' : Language
M : Type w
N : Type ?u.66568
P : Type ?u.66571
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
v : α → M
xs : Fin n → M
⊢ Realize (List.foldr (fun x x_1 => x ⊔ x_1) ⊥ []) v xs ↔ ∃ φ, φ ∈ [] ∧ Realize φ v xs
simp
no goals
case cons
L : Language
L' : Language
M : Type w
N : Type ?u.66568
P : Type ?u.66571
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
v : α → M
xs : Fin n → M
φ : BoundedFormula L α n
l : List (BoundedFormula L α n)
ih : Realize (List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l) v xs ↔ ∃ φ, φ ∈ l ∧ Realize φ v xs
⊢ Realize (List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (φ :: l)) v xs ↔ ∃ φ_1, φ_1 ∈ φ :: l ∧ Realize φ_1 v xs
simp_rw [List.foldr_cons, realize_sup, ih, exists_prop, List.mem_cons, or_and_right, exists_or,
  exists_eq_left]