diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index 2780fa5..f8dfbd9 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -361,23 +361,40 @@ export function getStyles(): string {
             text-align: right;
         }
         .vc-chain {
+            display: table;
+            width: 100%;
+            border-spacing: 0 0.25rem;
+            min-width: 0;
+        }
+        .counterexample-container .vc-chain {
             display: flex;
             flex-direction: column;
             gap: 0.25rem;
-            min-width: 0;
+        }
+        .counterexample-line {
+            overflow-wrap: anywhere;
         }
         .vc-line {
-            display: flex;
-            align-items: flex-start;
-            gap: 0.5rem;
-            min-width: 0;
-            padding: 0.0625rem 0.25rem;
-            border-radius: 3px;
+            display: table-row;
         }
-        .vc-line-content {
-            flex: 0 1 auto;
+        .vc-binder-cell,
+        .vc-predicate-cell {
+            display: table-cell;
             min-width: 0;
+            padding: 0.0625rem 0.25rem;
             overflow-wrap: anywhere;
+            vertical-align: top;
+        }
+        .vc-binder-cell {
+            min-height: 1.2em;
+            padding-right: 0.75rem;
+            color: var(--vscode-descriptionForeground);
+            white-space: nowrap;
+            width: 1%;
+        }
+        .vc-predicate-cell {
+            color: var(--vscode-editor-foreground);
+            width: 99%;
         }
         .vc-node {
             display: inline;
diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts
new file mode 100644
index 0000000..6d80f76
--- /dev/null
+++ b/client/src/webview/views/diagnostics/counterexample.ts
@@ -0,0 +1,25 @@
+import { renderHighlightedInlineExpression } from "../../highlighting";
+
+function getCounterexampleLines(counterexample: string): string[] {
+    return counterexample
+        .split("&&")
+        .map(assignment => assignment.trim())
+        .filter(Boolean);
+}
+
+export function renderCounterexample(counterexample: string): string {
+    const lines = getCounterexampleLines(counterexample);
+    if (lines.length === 0) return "";
+
+    return /*html*/`
+        <div class="container vc-container counterexample-container">
+            <div class="vc-chain">
+                ${lines.map(line => /*html*/`
+                    <div class="counterexample-line">
+                        <span class="vc-node">${renderHighlightedInlineExpression(line)}</span>
+                    </div>
+                `).join("")}
+            </div>
+        </div>
+    `;
+}
diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts
index c777a32..ac48c74 100644
--- a/client/src/webview/views/diagnostics/errors.ts
+++ b/client/src/webview/views/diagnostics/errors.ts
@@ -1,4 +1,5 @@
 import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton } from "../sections";
+import { renderCounterexample } from "./counterexample";
 import { renderVCImplication } from "./vc-implications";
 import type {
     ArgumentMismatchError,
@@ -36,7 +37,7 @@ const errorContentRenderers: ErrorRendererMap = {
     'refinement-error': (e: RefinementError) => /*html*/ `
         ${renderExpressionSection('Expected', e.expected)}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
-        ${e.counterexample ? renderExpressionSection('Counterexample', e.counterexample) : ''}
+        ${e.counterexample ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample)) : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/ `
         ${renderExpressionSection('Expected', e.expected)}
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index 928f14c..34a0333 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -1,5 +1,6 @@
 import type { VCImplication } from "../../../types/vc-implications";
 import { renderHighlightedInlineExpression } from "../../highlighting";
+import { escapeHtml } from "../../utils";
 
 type ChangeKind = "unchanged" | "removed" | "added";
 type DiffOperation<T> = { kind: ChangeKind; value: T };
@@ -7,23 +8,38 @@ type DiffOperation<T> = { kind: ChangeKind; value: T };
 const MIN_LINE_SIMILARITY = 0.3;
 const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu;
 const WHITESPACE_PATTERN = /^\s+$/u;
+const VC_LINE_SEPARATOR = "\t";
+
+function hasBinder(node: VCImplication): boolean {
+    return typeof node.name === "string" && node.name.length > 0;
+}
+
+function formatImplicationLine(node: VCImplication): string {
+    const binder = hasBinder(node) ? `∀${node.name}` : "";
+    const type = typeof node.type === "string" ? node.type : "";
+    return [binder, type, node.predicate].join(VC_LINE_SEPARATOR);
+}
+
+function parseImplicationLine(line: string): { binder: string; type: string; predicate: string } {
+    const [binder = "", type = "", predicate = ""] = line.split(VC_LINE_SEPARATOR);
+    return { binder, type, predicate };
+}
 
 function getImplicationLines(node: VCImplication): string[] {
     const lines: string[] = [];
     for (let current: VCImplication | null = node; current; current = current.next) {
-        if (
-            current.next
-            && (current.name === null || current.type === null || current.predicate === "true")
-        ) continue;
-        lines.push(current.predicate);
+        if (current.next && !hasBinder(current)) continue;
+        lines.push(formatImplicationLine(current));
     }
     return lines;
 }
 
-function renderVCLine(content: string, className = ""): string {
+export function renderVCLine(line: string, className = "", predicateContent?: string): string {
+    const { binder, type, predicate } = parseImplicationLine(line);
     return /*html*/`
         <div class="vc-line ${className}">
-            <div class="vc-line-content"><span class="vc-node">${content}</span></div>
+            <div class="vc-binder-cell"><span class="vc-node vc-binder" title="${type}">${escapeHtml(binder)}</span></div>
+            <div class="vc-predicate-cell"><span class="vc-node">${predicateContent ?? renderHighlightedInlineExpression(predicate)}</span></div>
         </div>
     `;
 }
@@ -158,16 +174,19 @@ function renderChangedDestinationLines(removed: string[], added: string[]): stri
     return alignChangedLines(removed, added)
         .map(([before, after]) => {
             if (after === undefined) return "";
-            if (before === undefined) return renderVCLine(renderChangedFragment(after));
-            const change = renderDestinationTokenDiff(before, after);
-            return renderVCLine(change.content, change.hasAddedContent ? "" : "vc-change-line");
+            if (before === undefined) return renderVCLine(after, "vc-change-line");
+            const change = renderDestinationTokenDiff(
+                parseImplicationLine(before).predicate,
+                parseImplicationLine(after).predicate,
+            );
+            return renderVCLine(after, change.hasAddedContent ? "" : "vc-change-line", change.content);
         })
         .join("");
 }
 
 export function renderImplication(node: VCImplication): string {
     return getImplicationLines(node)
-        .map(predicate => renderVCLine(renderHighlightedInlineExpression(predicate)))
+        .map(line => renderVCLine(line))
         .join("");
 }
 
@@ -185,7 +204,7 @@ export function renderImplicationChange(before: VCImplication, after: VCImplicat
     for (const operation of operations) {
         if (operation.kind === "unchanged") {
             flushChanges();
-            html += renderVCLine(renderHighlightedInlineExpression(operation.value));
+            html += renderVCLine(operation.value);
             continue;
         }
         changed[operation.kind].push(operation.value);
diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts
index 0942178..c2b76e6 100644
--- a/client/src/webview/views/diagnostics/vc-implications.ts
+++ b/client/src/webview/views/diagnostics/vc-implications.ts
@@ -22,7 +22,7 @@ function renderStepHeader(
 ): string {
     const currStep = stepCount - index;
     const simplification = current.simplification?.trim();
-    const label = escapeHtml(simplification || "Original");
+    const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original");
 
     return /*html*/`
         <div class="vc-step-header">