One could argue that the proof is just that all As are Xs where all Xs are Ds and therefore all As are Ds. This factors out the detail of choosing one path over

One could argue that the proof is just that all As are Xs where all Xs are Ds and therefore all As are Ds. This factors out the detail of choosing one path over the other. You have of course still to show that such an X exists and can use either pair of the axioms establishing this but as far as this proof is concerned both axiom pairs are really equivalent. So are this really two different proofs? How would one define equivalence between proofs to begin with? Isomorphic graphs of applied derivation rules?