diff --git a/ide/packages/common/src/BodyInfo.ts b/ide/packages/common/src/BodyInfo.ts
index ade3a83..72ddbb6 100644
--- a/ide/packages/common/src/BodyInfo.ts
+++ b/ide/packages/common/src/BodyInfo.ts
@@ -26,10 +26,6 @@ class BodyInfo {
     return this.oib.ambiguityErrors.length + this.oib.traitErrors.length;
   }
 
-  get exprs(): ExprIdx[] {
-    return _.map(this.oib.exprs, (_, idx) => idx);
-  }
-
   get name() {
     return this.oib.name;
   }
@@ -49,6 +45,7 @@ class BodyInfo {
   get tyInterner() {
     return this.oib.tys;
   }
+
   notHidden(hash: ObligationIdx): boolean {
     const o = this.getObligation(hash);
     if (o === undefined) {
@@ -57,8 +54,12 @@ class BodyInfo {
     return this.showHidden || isHiddenObl(o);
   }
 
+  exprs(): ExprIdx[] {
+    return _.map(this.oib.exprs, (_, idx) => idx);
+  }
+
   hasVisibleExprs() {
-    return _.some(this.exprs, idx => this.hasVisibleObligations(idx));
+    return _.some(this.exprs(), idx => this.hasVisibleObligations(idx));
   }
 
   hasVisibleObligations(idx: ExprIdx) {
diff --git a/ide/packages/panoptes/src/File.tsx b/ide/packages/panoptes/src/File.tsx
index 38e61b7..1740746 100644
--- a/ide/packages/panoptes/src/File.tsx
+++ b/ide/packages/panoptes/src/File.tsx
@@ -59,7 +59,7 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => {
         info={header}
         startOpen={openChildren}
         Children={() =>
-          _.map(bodyInfo.exprs, (i, idx) => <Expr idx={i} key={idx} />)
+          _.map(bodyInfo.exprs(), (i, idx) => <Expr idx={i} key={idx} />)
         }
       />
     </BodyInfoContext.Provider>
diff --git a/ide/packages/panoptes/src/Obligation.css b/ide/packages/panoptes/src/Obligation.css
index c47d216..e7a2166 100644
--- a/ide/packages/panoptes/src/Obligation.css
+++ b/ide/packages/panoptes/src/Obligation.css
@@ -1,3 +1,11 @@
 .ObligationCard > vscode-text-area {
     display: block;
 }
+
+.TreeAppObligationWrapper {
+    background-color: var(--vscode-editor-selectionHighlightBackground);
+    border-radius: 3px;
+    padding: 0.15em;
+
+    margin-bottom: 0.5em;
+}
\ No newline at end of file
diff --git a/ide/packages/panoptes/src/Obligation.tsx b/ide/packages/panoptes/src/Obligation.tsx
index 3079475..c4295cf 100644
--- a/ide/packages/panoptes/src/Obligation.tsx
+++ b/ide/packages/panoptes/src/Obligation.tsx
@@ -97,7 +97,9 @@ const ProofTreeWrapper = ({
     ) : tree === undefined ? (
       <NoTreeFound obligation={obligation} />
     ) : (
-      <TreeApp tree={tree} showHidden={bodyInfo.showHidden} />
+      <div className="TreeAppObligationWrapper">
+        <TreeApp tree={tree} showHidden={bodyInfo.showHidden} />
+      </div>
     );
 
   return content;
diff --git a/ide/packages/panoptes/src/TreeView/Subsets.tsx b/ide/packages/panoptes/src/TreeView/Subsets.tsx
index 0972888..619b2c5 100644
--- a/ide/packages/panoptes/src/TreeView/Subsets.tsx
+++ b/ide/packages/panoptes/src/TreeView/Subsets.tsx
@@ -50,18 +50,22 @@ export const RenderBottomUpSets = ({
         return null;
       }
 
+      const [hovered, setHovered] = useState(false);
+      const cn = classNames("FailingSet", { "is-hovered": hovered });
+
       // If there is only a single predicate, no need to provide all the
       // extra information around "grouped predicate sets".
       if (views.tree.length === 1) {
         return (
-          <DirRecursive
-            level={[views.tree[0].root]}
-            getNext={mkGetChildren(views.tree[0])}
-          />
+          <div className={cn}>
+            <DirRecursive
+              level={[views.tree[0].root]}
+              getNext={mkGetChildren(views.tree[0])}
+            />
+          </div>
         );
       }
 
-      const [hovered, setHovered] = useState(false);
       const onHover = () => {
         MiniBufferDataStore.set({
           kind: "argus-note",
@@ -80,7 +84,7 @@ export const RenderBottomUpSets = ({
       };
 
       return (
-        <div className={classNames("FailingSet", { "is-hovered": hovered })}>
+        <div className={cn}>
           <IcoComment onMouseEnter={onHover} onMouseLeave={onNoHover} />
           {_.map(views.tree, (leaf, i) => (
             <DirRecursive
@@ -94,21 +98,25 @@ export const RenderBottomUpSets = ({
     }
   );
 
-  const tail = _.slice(views, 3);
-  const argusViews = _.map(_.slice(views, 0, 3), (v, i) => (
-    <MkLevel {...v} key={i} />
-  ));
+  const argusRecommends = <MkLevel {..._.head(views)!} />;
+  const tail = _.tail(views);
+
+  const otherLabel = "Other failures";
   const fallbacks =
     tail.length === 0 ? null : (
       <CollapsibleElement
-        info={<span id="hidden-failure-list">Other failures ...</span>}
+        info={<span id="hidden-failure-list">{otherLabel} ...</span>}
         Children={() => _.map(tail, (v, i) => <MkLevel {...v} key={i} />)}
       />
     );
 
   return (
     <TreeAppContext.TreeRenderContext.Provider value={BottomUpRenderParams}>
-      <div id="recommended-failure-list">{argusViews}</div>
+      <p>
+        Argus recommends investigating these failed oblgiations. Click on ’
+        {otherLabel}‘ below to see other failed obligations.
+      </p>
+      <div id="recommended-failure-list">{argusRecommends}</div>
       {fallbacks}
     </TreeAppContext.TreeRenderContext.Provider>
   );
diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx
index 5cb3a84..f12b3e0 100644
--- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx
+++ b/ide/packages/panoptes/src/TreeView/TreeApp.tsx
@@ -49,8 +49,11 @@ const TreeApp = ({
   const tabs: [string, React.FC][] = [["Top Down", TopDown]];
 
   if (treeInfo.errorLeaves().length > 0) {
-    tabs.unshift(["Help Me", Erotisi]);
+    // Unshift to place this first
     tabs.unshift(["Bottom Up", FailedSubsets]);
+
+    // Push to place this last
+    tabs.push(["Help Me", Erotisi]);
   }
 
   // HACK: we shouldn't test for eval mode here but Playwright is off on the button click.
diff --git a/ide/packages/print/src/private/path.tsx b/ide/packages/print/src/private/path.tsx
index b1e31d5..347d5ef 100644
--- a/ide/packages/print/src/private/path.tsx
+++ b/ide/packages/print/src/private/path.tsx
@@ -79,11 +79,11 @@ export const PrintDefPath = ({ o }: { o: DefinedPath }) => {
           <Angled>
             <Toggle
               summary=".."
-              Children={() => <PrintPathSegment o={o[0]} />}
+              Children={() => <PrintDefPath o={o[0].inner} />}
             />
           </Angled>
         )}
-        Rest={() => <PrintSegments o={_.slice(o, 1)} />}
+        Rest={() => <PrintSegments o={_.tail(o)} />}
       />
     );
   };
@@ -192,7 +192,7 @@ const PrintInToggleableEnvironment = ({
   bypassToggle,
   Elem
 }: { bypassToggle: boolean; Elem: React.FC }) => {
-  // Use a metric of "type size" rather than inner lenght.
+  // Use a metric of "type size" rather than inner length.
   const useToggle = useContext(AllowToggle) && bypassToggle;
   return (
     // TODO: do we want to allow nested toggles?