---

Step * 3 1 of Lemma dm-neg-sq


1. I : Top
2. J : Top
3. v : Top
4. xs : Base
⊢ λx,y. (opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."meet" x y) 
~ λx,y. (opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."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
⊢ opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."meet" x y 
~ opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."meet" x y

---

Latex:

---

Latex:

1.  I  :  Top
2.  J  :  Top
3.  v  :  Top
4.  xs  :  Base
\mvdash{}  \mlambda{}x,y.  (opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."meet"  x  y) 
\msim{}  \mlambda{}x,y.  (opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."meet"  x  y)


By

---

Latex:
RepeatFor  2  (EqCD)

---

Home Index