---

Step * of Lemma fl-deq_wf

∀[I:fset(ℕ)]. (Deq(F(I)) ∈ EqDecider(Point(face_lattice(I))))
BY
{ ProveWfLemma }

1
1. I : fset(ℕ)
⊢ λx,y. (x==y) ∈ EqDecider(Point(face_lattice(I)))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  (Deq(F(I))  \mmember{}  EqDecider(Point(face\_lattice(I))))


By

---

Latex:
ProveWfLemma

---

Home Index