---

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


1. X : ℕ ⟶ Type
⊢ (⋂n:ℕ. partial(Unit ⋃ (Top × (X n)))) ⊆r partial(Unit ⋃ (Top × (⋂n:ℕ. (X n))))
BY
{ ((InstLemma `partial-type-continuous` [⌜λ2n.Unit ⋃ (Top × (X n))⌝]⋅ THENA Auto)
   THEN Assert ⌜partial(⋂n:ℕ. (Unit ⋃ (Top × (X n)))) ⊆r partial(Unit ⋃ (Top × (⋂n:ℕ. (X n))))⌝⋅
   THEN (Assert ⌜(⋂n:ℕ. (Unit ⋃ (Top × (X n)))) ⊆r (Unit ⋃ (Top × (⋂n:ℕ. (X n))))⌝⋅
   THENM ((Assert ⌜value-type(⋂n:ℕ. (Unit ⋃ (Top × (X n))))⌝⋅ THENA (Auto THEN InstConcl [⌜0⌝]⋅ THEN Auto))
          THEN Assert ⌜value-type(Unit ⋃ (Top × (⋂n:ℕ. (X n))))⌝⋅
          THEN Auto)
   )
   THEN InstLemma `strong-continuous-b-union` [⌜λ2T.Unit⌝;⌜λ2T.Top × T⌝]⋅
   THEN Auto
   THEN Try (Complete ((ProveContinuous THEN Auto)))
   THEN (D 0 THEN Auto)
   THEN RenameVar `x' (-1)
   THEN Assert ⌜ispair(x) = tt ∧ ispair(x) = ff⌝⋅
   THEN Auto
   THEN Try (Complete ((GenConcl ⌜x = p ∈ (Top × S)⌝⋅ THEN Auto THEN D (-2) THEN Reduce 0 THEN Auto)))
   THEN Try (Complete ((GenConcl ⌜x = p ∈ Unit⌝⋅ THEN Auto THEN D (-2) THEN Reduce 0 THEN Auto)))) }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `partial-type-continuous`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.Unit  \mcup{}  (Top  \mtimes{}  (X  n))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}partial(\mcap{}n:\mBbbN{}.  (Unit  \mcup{}  (Top  \mtimes{}  (X  n))))  \msubseteq{}r  partial(Unit  \mcup{}  (Top  \mtimes{}  (\mcap{}n:\mBbbN{}.  (X  n))))\mkleeneclose{}\mcdot{}
  THEN  (Assert  \mkleeneopen{}(\mcap{}n:\mBbbN{}.  (Unit  \mcup{}  (Top  \mtimes{}  (X  n))))  \msubseteq{}r  (Unit  \mcup{}  (Top  \mtimes{}  (\mcap{}n:\mBbbN{}.  (X  n))))\mkleeneclose{}\mcdot{}
  THENM  ((Assert  \mkleeneopen{}value-type(\mcap{}n:\mBbbN{}.  (Unit  \mcup{}  (Top  \mtimes{}  (X  n))))\mkleeneclose{}\mcdot{}
                  THENA  (Auto  THEN  InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  )
                THEN  Assert  \mkleeneopen{}value-type(Unit  \mcup{}  (Top  \mtimes{}  (\mcap{}n:\mBbbN{}.  (X  n))))\mkleeneclose{}\mcdot{}
                THEN  Auto)
  )
  THEN  InstLemma  `strong-continuous-b-union`  [\mkleeneopen{}\mlambda{}\msubtwo{}T.Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}T.Top  \mtimes{}  T\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((ProveContinuous  THEN  Auto)))
  THEN  (D  0  THEN  Auto)
  THEN  RenameVar  `x'  (-1)
  THEN  Assert  \mkleeneopen{}ispair(x)  =  tt  \mwedge{}  ispair(x)  =  ff\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((GenConcl  \mkleeneopen{}x  =  p\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  (-2)  THEN  Reduce  0  THEN  Auto)))
  THEN  Try  (Complete  ((GenConcl  \mkleeneopen{}x  =  p\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  (-2)  THEN  Reduce  0  THEN  Auto))))

---

Home Index