---

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


1. I : Top
2. J : Top
3. v : Top
⊢ λxs.reduce(λx,y. (face_lattice(I)."meet" x y);1;λx.case x of inl(a) => (a=1) | inr(a) => (a=0)"(xs))"(v) 
~ λxs.reduce(λx,y. (face_lattice(J)."meet" x y);1;λx.case x of inl(a) => (a=1) | inr(a) => (a=0)"(xs))"(v)
BY
{ RepeatFor 3 ((EqCD THEN Try (Trivial))) }

1
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)

2
1. I : Top
2. J : Top
3. v : Top
4. xs : Base
⊢ 1 ~ 1

---

Latex:

---

Latex:

1.  I  :  Top
2.  J  :  Top
3.  v  :  Top
\mvdash{}  \mlambda{}xs.reduce(\mlambda{}x,y.  (face\_lattice(I)."meet"  x 
                                        y);1;\mlambda{}x.case  x  of  inl(a)  =>  (a=1)  |  inr(a)  =>  (a=0)"(xs))"(v) 
\msim{}  \mlambda{}xs.reduce(\mlambda{}x,y.  (face\_lattice(J)."meet"  x 
                                        y);1;\mlambda{}x.case  x  of  inl(a)  =>  (a=1)  |  inr(a)  =>  (a=0)"(xs))"(v)


By

---

Latex:
RepeatFor  3  ((EqCD  THEN  Try  (Trivial)))

---

Home Index