Thm* 
Alph,States:Type, n:NDA(Alph;States). I(n) 
States
Thm* A:Type, B:(A
Type), p:a:A
B(a). 2of(p) B(1of(p))
Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A
| NDA_init |
Def I(n) == 1of(2of(n))
Thm* |
| pi2 |
Def 2of(t) == t.2
Thm* |
| pi1 |
Def 1of(t) == t.1
Thm* |
About:
 |  |  |  |  |  |  |