intro x hx
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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
⊢ Function.funEqOn (fvar? p) (fun x => ε (fvListingInv p (fvListing p x))) ε
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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
x : μ
hx : fvar? p x
⊢ (fun x => ε (fvListingInv p (fvListing p x))) x = ε x