---

Step * of Lemma pi-rep-decompose

∀[P:pi_term()]. P = pirep(pirep-body(P)) ∈ pi_term() supposing ↑pirep?(P)
BY
{ (D 0 THENA Auto)
THEN SimpleDatatypeInduction  1
THEN Auto }

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()].  P  =  pirep(pirep-body(P))  supposing  \muparrow{}pirep?(P)


By

---

Latex:
(D  0  THENA  Auto)
THEN  SimpleDatatypeInduction    1
THEN  Auto

---

Home Index