---

Step * of Lemma tcWO-induction

∀[T:Type]. ∀[>:T ⟶ T ⟶ ℙ].  ∀[Q:T ⟶ ℙ]. TI(T;x,y.>[x;y];t.Q[t]) supposing tcWO(T;x,y.>[x;y])
BY
{ (InstLemma `AF-induction2` []
   THEN RepeatFor 3 (ParallelLast')
   THEN D -1
   THEN Auto
   THEN D -1
   THEN Unfold `almost-full` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[>:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  TI(T;x,y.>[x;y];t.Q[t])  supposing  tcWO(T;x,y.>[x;y])


By

---

Latex:
(InstLemma  `AF-induction2`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  D  -1
  THEN  Auto
  THEN  D  -1
  THEN  Unfold  `almost-full`  0
  THEN  Auto)

---

Home Index