---

Step * of Lemma W-uwellfounded_witness

λF.fix(F) ∈ ∀[A:Type]. ∀[B:A ⟶ Type].  uWellFnd(W(A;a.B[a]);w1,w2.w1 <  w2)
BY
{ (RepUR ``uall uwellfounded`` 0
   THEN RepeatFor 3 ((MemTypeCD THENA Auto))
   THEN BetterExt
   THEN Auto
   THEN RenameVar `f' (-2)
   THEN RenameVar `w' (-1)
   THEN MoveToConcl (-1)) }

1
1. A : Type
2. B : A ⟶ Type
3. P : W(A;a.B[a]) ⟶ ℙ
4. f : ⋂j:W(A;a.B[a]). ((⋂k:{k:W(A;a.B[a])| k <  j} . P[k]) ⇒ P[j])
⊢ ∀w:W(A;a.B[a]). (fix(f) ∈ P[w])

---

Latex:

---

Latex:
\mlambda{}F.fix(F)  \mmember{}  \mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    uWellFnd(W(A;a.B[a]);w1,w2.w1  <    w2)


By

---

Latex:
(RepUR  ``uall  uwellfounded``  0
  THEN  RepeatFor  3  ((MemTypeCD  THENA  Auto))
  THEN  BetterExt
  THEN  Auto
  THEN  RenameVar  `f'  (-2)
  THEN  RenameVar  `w'  (-1)
  THEN  MoveToConcl  (-1))

---

Home Index