---

Step * of Lemma sub-corec-family

∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].
  corec-family(H) ⊆ H corec-family(H) supposing type-family-continuous{i:l}(P;H)
BY
{ (Auto
   THEN Unfold `type-family-continuous` -1
   THEN Unfold `corec-family` 0
   THEN (InstHyp [⌜λn.(H^n (λp.Top))⌝] (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Using [`G',⌜⋂n:ℕ. H (H^n (λp.Top))⌝] (BLemma `sub-family_transitivity`)⋅
   THEN Auto) }

1
1. P : Type
2. H : (P ⟶ Type) ⟶ P ⟶ Type
3. ∀[X:ℕ ⟶ P ⟶ Type]. ⋂n:ℕ. H (X n) ⊆ H ⋂n:ℕ. X n
4. ⋂n:ℕ. H (H^n (λp.Top)) ⊆ H ⋂n:ℕ. H^n (λp.Top)
⊢ ⋂n:ℕ. H^n (λp.Top) ⊆ ⋂n:ℕ. H (H^n (λp.Top))

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[H:(P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].
    corec-family(H)  \msubseteq{}  H  corec-family(H)  supposing  type-family-continuous\{i:l\}(P;H)


By

---

Latex:
(Auto
  THEN  Unfold  `type-family-continuous`  -1
  THEN  Unfold  `corec-family`  0
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}n.(H\^{}n  (\mlambda{}p.Top))\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Using  [`G',\mkleeneopen{}\mcap{}n:\mBbbN{}.  H  (H\^{}n  (\mlambda{}p.Top))\mkleeneclose{}]  (BLemma  `sub-family\_transitivity`)\mcdot{}
  THEN  Auto)

---

Home Index