---

Step * of Lemma strong-continuous-tag-case

∀[z:Atom]. ∀[F:Type ⟶ Type].  Continuous+(T.z:F[T]) supposing Continuous+(T.F[T])
BY
{ (Auto THEN Unfold `tag-case` 0 THEN BLemma `strong-continuous-depproduct`  THEN Auto THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[z:Atom].  \mforall{}[F:Type  {}\mrightarrow{}  Type].    Continuous+(T.z:F[T])  supposing  Continuous+(T.F[T])


By

---

Latex:
(Auto  THEN  Unfold  `tag-case`  0  THEN  BLemma  `strong-continuous-depproduct`    THEN  Auto  THEN  AutoSplit)

---

Home Index