---

Step * of Lemma deq-mFO_wf

deq-mFO() ∈ EqDecider(mFOL())
BY
{ (Unfold `deq` 0 THEN ProveWfLemma THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. x : mFOL()@i
2. y : mFOL()@i
3. x = y ∈ mFOL()@i
⊢ ↑eq_mFO(x;y)

2
1. x : mFOL()@i
2. y : mFOL()@i
3. ↑eq_mFO(x;y)@i
⊢ x = y ∈ mFOL()

---

Latex:


deq-mFO()  \mmember{}  EqDecider(mFOL())


By

(Unfold  `deq`  0  THEN  ProveWfLemma  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index