---

Step * of Lemma ptuple-continuous

∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)].  type-family-continuous{i:l}(P;λX.ptuple(lbl,p.a[lbl;p];X))
BY
{ (Auto
   THEN RepeatFor 2 (((D 0 THEN Auto) THEN Reduce 0))
   THEN All (RepUR ``isect-family``)
   THEN (D 0 THENA Auto)
   THEN (Assert ∀n:ℕ. (x ∈ ptuple(lbl,p.a[lbl;p];λp.(X n p)) p) BY
               ((D 0 THENA Auto)
                THEN (Assert x ∈ ptuple(lbl,p.a[lbl;p];X n) p BY
                            Auto)
                THEN RepUR ``ptuple let`` -1
                THEN RepUR ``ptuple let`` 0
                THEN Auto))
   THEN (Assert x ~ <fst(x), snd(x)> BY
               ((GenConcl ⌜x = z ∈ (ptuple(lbl,p.a[lbl;p];X 0) p)⌝⋅ THENA Auto)
                THEN RepUR ``ptuple`` -2
                THEN D -2
                THEN Reduce 0
                THEN Auto))
   THEN (Assert fst(x) ∈ {lbl:Atom| 0 < ||a[lbl;p]||}  BY
               ((GenConcl ⌜x = z ∈ (ptuple(lbl,p.a[lbl;p];X 0) p)⌝⋅ THENA Auto)
                THEN RepUR ``ptuple`` -2
                THEN D -2
                THEN Reduce 0
                THEN Auto))
   THEN HypSubst' (-2) (-3)
   THEN HypSubst' (-2) 0
   THEN RepUR ``ptuple`` 0
   THEN (MemCD THENA Auto)
   THEN Try (Trivial)) }

1
.....subterm..... T:t
2:n
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. X : ℕ ⟶ P ⟶ Type
4. p : P
5. x : ⋂n:ℕ. (ptuple(lbl,p.a[lbl;p];X n) p)
6. ∀n:ℕ. (<fst(x), snd(x)> ∈ ptuple(lbl,p.a[lbl;p];λp.(X n p)) p)
7. x ~ <fst(x), snd(x)>
8. fst(x) ∈ {lbl:Atom| 0 < ||a[lbl;p]||} 
⊢ snd(x) ∈ tuple-type(map(λx.case x
                              of inl(y) =>
                              case y of inl(p) => ⋂n:ℕ. (X n p) | inr(p) => (⋂n:ℕ. (X n p)) List
                              | inr(E) =>
                              E;a[fst(x);p]))

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].
    type-family-continuous\{i:l\}(P;\mlambda{}X.ptuple(lbl,p.a[lbl;p];X))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (((D  0  THEN  Auto)  THEN  Reduce  0))
  THEN  All  (RepUR  ``isect-family``)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mforall{}n:\mBbbN{}.  (x  \mmember{}  ptuple(lbl,p.a[lbl;p];\mlambda{}p.(X  n  p))  p)  BY
                          ((D  0  THENA  Auto)
                            THEN  (Assert  x  \mmember{}  ptuple(lbl,p.a[lbl;p];X  n)  p  BY
                                                    Auto)
                            THEN  RepUR  ``ptuple  let``  -1
                            THEN  RepUR  ``ptuple  let``  0
                            THEN  Auto))
  THEN  (Assert  x  \msim{}  <fst(x),  snd(x)>  BY
                          ((GenConcl  \mkleeneopen{}x  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  RepUR  ``ptuple``  -2
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (Assert  fst(x)  \mmember{}  \{lbl:Atom|  0  <  ||a[lbl;p]||\}    BY
                          ((GenConcl  \mkleeneopen{}x  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  RepUR  ``ptuple``  -2
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  HypSubst'  (-2)  (-3)
  THEN  HypSubst'  (-2)  0
  THEN  RepUR  ``ptuple``  0
  THEN  (MemCD  THENA  Auto)
  THEN  Try  (Trivial))

---

Home Index