Step
*
1
2
of Lemma
church-zero_wf2
cZ ∈ church-inductive{i:l}(cZ)
BY
{ BLemma `church-iZ` }
Latex:
Latex:
cZ  \mmember{}  church-inductive\{i:l\}(cZ)
By
Latex:
BLemma  `church-iZ`
Home
Index