thm (addcan () () (<-> (= (+ B A) (+ C A)) (= B C)) x (0) B addeq2 x (0) C addeq2 eqeq12d (= B C) bibi1d B pa_ax3 C pa_ax3 eqeq12 #B y pa_ax4 C y pa_ax4

