Argument Graph Layout

• Premises now flow in derivation order. The argument graph view used to stack every top-level premise in a single column, so reading even a moderately sized argument meant panning up and down a tall list. Premises are now laid out in rows that follow the chain of inference: the conclusion sits on top, the premises that feed it sit below, the premises that feed those sit below them, and so on. Reading top-to-bottom roughly traces the argument back to its base premises.
• Constraint premises sit beside the work they modify. Premises that constrain shape rather than derive a conclusion (e.g., A ∧ B, (U ∧ T) ∨ R) are placed on the row of the deepest implication they share variables with, so they appear next to the inference step they bear on instead of floating on their own.
• Visually demoted singleton row. Premises that assert a single variable, and constraint premises that share no variables with the chain, are gathered onto a final row at the bottom and rendered with reduced contrast and a muted border. They're still visible, just out of the way.
• Tidier within-row ordering. Within each row, premises are arranged so they sit roughly under the premises they feed, reducing edge crossings between nested expressions across rows.

Selection Highlighting

• Selecting a variable highlights its other appearances. Click a variable node in any premise and dotted overlay edges appear from that variable to every other variable across other premises that references the same claim. Deselecting (or clicking an edge / empty space) clears the overlay.
• Overlay edges are styled by role. Each match is colored according to the role the matched variable plays in its own premise — antecedent, consequent, asserted (in a constraint or singleton), or counter (when the variable sits under an odd number of NOT operators on its path to the premise root). Counter edges additionally render a small ¬ glyph midway along the line.
• IFF children read as consequent on both sides. Variables on either side of an IFF are treated as consequent rather than splitting into "antecedent" / "consequent" branches, since the equivalence is symmetric.

Other Fixes

• Review section icon margin. A small icon-margin issue in the sidebar's Review section that caused the icon to inherit unwanted spacing has been corrected.