have : M ⊧ₘ “∀ x y z, x = y → y = z → x = z” := H.realize (Theory.eqAxiom.trans (L := L))
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b c : M
⊢ eqv L a b → eqv L b c → eqv L a c
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b c : M
this : M ⊧ₘ (“∀' ∀' ∀' (#2 = #1 → (#1 = #0 → #2 = #0))”)
⊢ eqv L a b → eqv L b c → eqv L a c