---

Step * 2 of Lemma deq-mFO_wf


1. x : mFOL()@i
2. y : mFOL()@i
3. ↑eq_mFO(x;y)@i
⊢ x = y ∈ mFOL()
BY
{ (RWO "assert-eq_mFO" (-1) THEN Auto)⋅ }

---

Latex:



1.  x  :  mFOL()@i
2.  y  :  mFOL()@i
3.  \muparrow{}eq\_mFO(x;y)@i
\mvdash{}  x  =  y


By

(RWO  "assert-eq\_mFO"  (-1)  THEN  Auto)\mcdot{}

---

Home Index