---

Step * 1 1 2 1 1 of Lemma free-dma-hom-is-lattice-hom


1. v : record(x.Top)
2. F : Top
3. v = v["neg" := F] ∈ Top
⊢ Top ⊆r record(x.Top)
BY
{ BLemma `top-subtype-record` }

---

Latex:

---

Latex:

1.  v  :  record(x.Top)
2.  F  :  Top
3.  v  =  v["neg"  :=  F]
\mvdash{}  Top  \msubseteq{}r  record(x.Top)


By

---

Latex:
BLemma  `top-subtype-record`

---

Home Index