---

Step * of Lemma pi-option-decompose

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

---

Latex:

---

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


By

---

Latex:
(D  0  THENA  Auto)
THEN  SimpleDatatypeInduction    1
THEN  Auto\mcdot{}

---

Home Index