---

Step * 2 of Lemma fl-morph-id


1. I : fset(ℕ)
2. x : names(I)
3. ((λx.x) (x=0)) = ((λj.dM-to-FL(I;¬(1 j))) x) ∈ Point(face-lattice(names(I);NamesDeq))
⊢ (x=1) = dM-to-FL(I;<x>) ∈ Point(face_lattice(I))
BY
{ (RWO "dM-to-FL-inc dM-to-FL-opp" 0 THEN Try ((Folds ``fl1 fl0`` 0 THEN EqCD)) THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  names(I)
3.  ((\mlambda{}x.x)  (x=0))  =  ((\mlambda{}j.dM-to-FL(I;\mneg{}(1  j)))  x)
\mvdash{}  (x=1)  =  dM-to-FL(I;<x>)


By

---

Latex:
(RWO  "dM-to-FL-inc  dM-to-FL-opp"  0  THEN  Try  ((Folds  ``fl1  fl0``  0  THEN  EqCD))  THEN  Auto)

---

Home Index