---

Step * of Lemma retractible_wf

∀[T:Type]. retractible(T) ∈ ℙ supposing T ⊆r Base
BY
{ (Auto
   THEN Unfold `retractible` 0
   THEN RepeatFor 3 ((MemCD THENW Auto))
   THEN Try (BLemma `equal-wf-base-T`)
   THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  retractible(T)  \mmember{}  \mBbbP{}  supposing  T  \msubseteq{}r  Base


By

---

Latex:
(Auto
  THEN  Unfold  `retractible`  0
  THEN  RepeatFor  3  ((MemCD  THENW  Auto))
  THEN  Try  (BLemma  `equal-wf-base-T`)
  THEN  Try  (Complete  (Auto)))

---

Home Index