---

Step * of Lemma mutual-corec-ext2

∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
  (mutual-corec(T.F[T]) ≡ F[mutual-corec(T.F[T])]) supposing 
     ((∀i,j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i)) and 
     k-Monotone(T.F[T]))
BY
{ (InstLemma `mutual-corec-ext` [] THEN RepeatFor 2 (ParallelLast') THEN Auto THEN BackThruSomeHyp THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].
    (mutual-corec(T.F[T])  \mequiv{}  F[mutual-corec(T.F[T])])  supposing 
          ((\mforall{}i,j:\mBbbN{}k.  \mforall{}Z:\mBbbN{}k  {}\mrightarrow{}  Type.    Continuous(X.F[\mlambda{}i.if  (i  =\msubz{}  j)  then  X  else  Z  i  fi  ]  i))  and 
          k-Monotone(T.F[T]))


By

---

Latex:
(InstLemma  `mutual-corec-ext`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  EAuto  1)

---

Home Index