Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
p : Semiformula L μ n
h : Function.funEqOn (fun x => x ∈ p.fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
induction p using Semiformula.rec'
Proof state after:
case hverum
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊤.fvarList) ε ε'
⊢ (Eval s e ε) ⊤ ↔ (Eval s e ε') ⊤

case hfalsum
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊥.fvarList) ε ε'
⊢ (Eval s e ε) ⊥ ↔ (Eval s e ε') ⊥

case hrel
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r✝ v✝).fvarList) ε ε'
⊢ (Eval s e ε) (rel r✝ v✝) ↔ (Eval s e ε') (rel r✝ v✝)

case hnrel
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r✝ v✝).fvarList) ε ε'
⊢ (Eval s e ε) (nrel r✝ v✝) ↔ (Eval s e ε') (nrel r✝ v✝)

case hand
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
a✝ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q✝.fvarList) ε ε' → ((Eval s e ε) q✝ ↔ (Eval s e ε') q✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p✝ ⋏ q✝).fvarList) ε ε'
⊢ (Eval s e ε) (p✝ ⋏ q✝) ↔ (Eval s e ε') (p✝ ⋏ q✝)

case hor
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
a✝ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q✝.fvarList) ε ε' → ((Eval s e ε) q✝ ↔ (Eval s e ε') q✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p✝ ⋎ q✝).fvarList) ε ε'
⊢ (Eval s e ε) (p✝ ⋎ q✝) ↔ (Eval s e ε') (p✝ ⋎ q✝)

case hall
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p✝).fvarList) ε ε'
⊢ (Eval s e ε) (∀' p✝) ↔ (Eval s e ε') (∀' p✝)

case hex
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p✝).fvarList) ε ε'
⊢ (Eval s e ε) (∃' p✝) ↔ (Eval s e ε') (∃' p✝)