---

Step * of Lemma W-wfdd

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:W(A;a.B[a])].  coW-wfdd(a.B[a];w)
BY
{ (InstLemma `sq_stable__coW-wfdd` []⋅
   THEN RepeatFor 3 (ParallelLast')
   THEN Unhide
   THEN RepUR ``W param-W`` -2
   THEN Fold `coW` (-2)
   THEN D -2
   THEN Unhide
   THEN Thin (-1)
   THEN (D 0 THENA Auto)
   THEN D -1) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. ∀path:Path. (StepAgree(path 0;⋅;w) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
5. p : n:ℕ ⟶ copath(a.B[a];w)
6. ∀i:ℕ
     ((copath-length(p i) = i ∈ ℤ) ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ) ⇒ copathAgree(a.B[a];w;p i;p (i + 1)))
⊢ ↓∃i:ℕ. (¬(copath-length(p i) = i ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:W(A;a.B[a])].    coW-wfdd(a.B[a];w)


By

---

Latex:
(InstLemma  `sq\_stable\_\_coW-wfdd`  []\mcdot{}
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Unhide
  THEN  RepUR  ``W  param-W``  -2
  THEN  Fold  `coW`  (-2)
  THEN  D  -2
  THEN  Unhide
  THEN  Thin  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1)

---

Home Index