---

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


1. v : record(x.Top)
2. F : Top
⊢ v = v["neg" := F] ∈ record(x.Top)
BY
{ (SubsumeC ⌜Top⌝⋅ THEN Auto) }

1
1. v : record(x.Top)
2. F : Top
3. v = v["neg" := F] ∈ Top
⊢ Top ⊆r record(x.Top)

---

Latex:

---

Latex:

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


By

---

Latex:
(SubsumeC  \mkleeneopen{}Top\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index