---

Step * 1 of Lemma dM-deq_wf


1. I : fset(ℕ)
⊢ free-dml-deq(names(I);NamesDeq) ∈ EqDecider(Point(dM(I)))
BY
{ InferEqualType }

1
1. I : fset(ℕ)
⊢ EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq))) = EqDecider(Point(dM(I))) ∈ Type

2
1. I : fset(ℕ)
2. EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq))) = EqDecider(Point(dM(I))) ∈ Type
⊢ free-dml-deq(names(I);NamesDeq) ∈ EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
\mvdash{}  free-dml-deq(names(I);NamesDeq)  \mmember{}  EqDecider(Point(dM(I)))


By

---

Latex:
InferEqualType

---

Home Index