---

Step * of Lemma co-W-ext

∀[A:Type]. ∀[B:A ⟶ Type].  co-W(A;a.B[a]) ≡ a:A × (B[a] ⟶ co-W(A;a.B[a]))
BY
{ xxx(Auto
      THEN Unfold `co-W` 0
      THEN BLemma `corec-ext`
      THEN Auto
      THEN BLemma `continuous-monotone-depproduct`
      THEN Auto
      THEN (GenConcl ⌜a = z ∈ A⌝⋅ THENA (Auto THEN UseWitness ⌜0⌝⋅ THEN Auto))
      THEN ThinVar `a')xxx }

1
1. A : Type
2. B : A ⟶ Type
3. X : ℕ ⟶ Type
4. z : A
⊢ (⋂n:ℕ. (B[z] ⟶ (X n))) ⊆r (B[z] ⟶ (⋂n:ℕ. (X n)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    co-W(A;a.B[a])  \mequiv{}  a:A  \mtimes{}  (B[a]  {}\mrightarrow{}  co-W(A;a.B[a]))


By

---

Latex:
xxx(Auto
        THEN  Unfold  `co-W`  0
        THEN  BLemma  `corec-ext`
        THEN  Auto
        THEN  BLemma  `continuous-monotone-depproduct`
        THEN  Auto
        THEN  (GenConcl  \mkleeneopen{}a  =  z\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  UseWitness  \mkleeneopen{}0\mkleeneclose{}\mcdot{}  THEN  Auto))
        THEN  ThinVar  `a')xxx

---

Home Index