dnr Show Code edit
thm (dnr () () (-> ph (-. (-. ph)))
(-. ph) dn a3i)
(-> ph (-. (-. ph)))
edit