Step |
Hyp |
Ref |
Expression |
1 |
|
prstcnid.c |
Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- |
2 |
|
prstcnid.k |
|
3 |
|
prstcoc.oc |
|
4 |
|
ocid |
|
5 |
|
slotsdifocndx |
|
6 |
5
|
simpli |
|
7 |
5
|
simpri |
|
8 |
1 2 4 6 7
|
prstcnid |
|
9 |
3 8
|
eqtrd |
|