---

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


1. I : Top
2. J : Top
3. v : Top
4. xs : Base
⊢ λx,y. (face_lattice(I)."meet" x y) ~ λx,y. (face_lattice(J)."meet" x y)
BY
{ RepeatFor 2 (EqCD) }

1
1. I : Top
2. J : Top
3. v : Top
4. xs : Base
5. x : Base
6. y : Base
⊢ face_lattice(I)."meet" x y ~ face_lattice(J)."meet" x y

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  2  (EqCD)

---

Home Index