Step 
*
 of Lemma 
pioption?_wf
∀[v:pi_term()]. (pioption?(v) ∈ 𝔹)
BY
 
{ DepprodCoDatatypeRecognizerWf }
 
Latex: 
Latex:
\mforall{}[v:pi\_term()].  (pioption?(v)  \mmember{}  \mBbbB{})
 By 
Latex:
DepprodCoDatatypeRecognizerWf
Home
Index