com4r Show Code edit
## Commute Antecedents (Rotate Right)
thm (com4r () (1 (-> ph (-> ps (-> ch (-> th ta)))))
(-> th (-> ph (-> ps (-> ch ta))))
1 com4l com4t)
(-> th (-> ph (-> ps (-> ch ta))))
edit