---

Step * 1 2 of Lemma is-list-if-has-value-ext


1. X : ℕ ⟶ Type
⊢ partial(Unit ⋃ (Top × (⋂n:ℕ. (X n)))) ⊆r (⋂n:ℕ. partial(Unit ⋃ (Top × (X n))))
BY
{ ((BLemma `subtype_rel_isect` THEN Auto)
   THEN (Assert ⌜(Unit ⋃ (Top × (⋂n:ℕ. (X n)))) ⊆r (Unit ⋃ (Top × (X n)))⌝⋅ THENA Auto)
   THEN (Assert ⌜value-type(Unit ⋃ (Top × (⋂n:ℕ. (X n))))⌝⋅ THENA Auto)
   THEN Assert ⌜value-type(Unit ⋃ (Top × (X n)))⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  \mBbbN{}  {}\mrightarrow{}  Type
\mvdash{}  partial(Unit  \mcup{}  (Top  \mtimes{}  (\mcap{}n:\mBbbN{}.  (X  n))))  \msubseteq{}r  (\mcap{}n:\mBbbN{}.  partial(Unit  \mcup{}  (Top  \mtimes{}  (X  n))))


By

---

Latex:
((BLemma  `subtype\_rel\_isect`  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}(Unit  \mcup{}  (Top  \mtimes{}  (\mcap{}n:\mBbbN{}.  (X  n))))  \msubseteq{}r  (Unit  \mcup{}  (Top  \mtimes{}  (X  n)))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}value-type(Unit  \mcup{}  (Top  \mtimes{}  (\mcap{}n:\mBbbN{}.  (X  n))))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}value-type(Unit  \mcup{}  (Top  \mtimes{}  (X  n)))\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index