intro h a
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p) → ∀ (x : M), (Eval inst✝ (x :> e) ε) p
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
a : M
⊢ (Eval inst✝ (a :> e) ε) p