---

Step * of Lemma pi-new-decompose

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

---

Latex:

---

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


By

---

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

---

Home Index