Thm* p:PM{i}. p.s
(p)
Thm* B:(A
Type), p:a:A
B(a). 2of(p)
B(1of(p))
Thm* B:(A
Type), p:a:A
B(a). 1of(p)
A
| tm_s |
Def p.s == 1of(2of(2of(2of(2of(2of(p))))))
Thm* |
| pi2 |
Def 2of(t) == t.2
Thm* |
| pi1 |
Def 1of(t) == t.1
Thm* |