Nuprl Lemma : aa_max_ltree_wf
[t:aa_ltree(
)]. (aa_max_ltree(t) 
?)
Proof not projected
Error : references
\mforall{}[t:aa\_ltree(\mBbbZ{})]. (aa\_max\_ltree(t) \mmember{} \mBbbZ{}?)
Date html generated:
2013_03_20-AM-11_02_19
Last ObjectModification:
2012_11_27-AM-10_32_46
Home
Index