---

Step * of Lemma pi-comm-decompose

∀[P:pi_term()]. P = picomm(picomm-pre(P);picomm-body(P)) ∈ pi_term() supposing ↑picomm?(P)
BY
{ (D 0 THENA Auto)
THEN (MoveToConcl (-1) THEN BLemma `pi_term-induction` THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(D  0  THENA  Auto)
THEN  (MoveToConcl  (-1)  THEN  BLemma  `pi\_term-induction`  THEN  Auto)

---

Home Index