dni Show Code edit
thm (dni () (1 (-. (-. ph))) ph
1 ph dn ax-mp)
ph
edit