---

Step * 1 of Lemma dM-to-FL-sq


1. I : Top
2. J : Top
3. v : Top
⊢ λx,y. (face_lattice(I)."join" x y) ~ λx,y. (face_lattice(J)."join" x y)
BY
{ (RepeatFor 2 (EqCD)
   THEN RepeatFor 6 (RW (SubC (AddrC [1;1;1] UnfoldTopAbC)) 0)
   THEN RepUR ``union-deq`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Top
2.  J  :  Top
3.  v  :  Top
\mvdash{}  \mlambda{}x,y.  (face\_lattice(I)."join"  x  y)  \msim{}  \mlambda{}x,y.  (face\_lattice(J)."join"  x  y)


By

---

Latex:
(RepeatFor  2  (EqCD)
  THEN  RepeatFor  6  (RW  (SubC  (AddrC  [1;1;1]  UnfoldTopAbC))  0)
  THEN  RepUR  ``union-deq``  0
  THEN  Auto)

---

Home Index