---

Step * of Lemma pi-par-decompose

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

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()].  P  =  pipar(pipar-left(P);pipar-right(P))  supposing  \muparrow{}pipar?(P)


By

---

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

---

Home Index