 The point of isolating Id- and Cut-inductivity here, however, has less to do with matters of truth (on which, and for further references to Girard on which, see further Hösli and Jäger 1994) than with uniqueness and existence—not that the semantical issues are unconnected with this, of course. The former link is perhaps already clear. At the last step of establishing Id-inductivity for →, above, we passed from φ → ψ, φ ≻ ψ, obtained by (→ Left), to φ → ψ ≻ φ → ψ, by (→ Left): but this is just what the uniqueness proof in the reduplicated sequent calculus would do, except that the final step would be an application of (→′ Right) and would establish φ → ψ ≻ φ →′ ψ, with the converse proved by interchanging the rules used for → and →′.