diff --git a/lib/til.ex b/lib/til.ex
index 590214d..1685e74 100644
--- a/lib/til.ex
+++ b/lib/til.ex
@@ -1373,87 +1373,131 @@ defmodule Tdd.Algo do
 
   # This function is correct and does not need to be changed.
   defp do_apply(op_name, op_lambda, u1_id, u2_id) do
-    with {:ok, u1_details} <- Store.get_node(u1_id),
-         {:ok, u2_details} <- Store.get_node(u2_id) do
-      cond do
-        (u1_details == :true_terminal or u1_details == :false_terminal) and
-            (u2_details == :true_terminal or u2_details == :false_terminal) ->
-          if op_lambda.(u1_details, u2_details) == :true_terminal,
-            do: Store.true_node_id(),
-            else: Store.false_node_id()
+    if u1_id == u2_id do
+      # If both nodes are the same, the result of the operation is idempotent.
+      u1_id
+    else
+      # The core logic for distinct nodes.
+      with {:ok, u1_details} <- Store.get_node(u1_id),
+           {:ok, u2_details} <- Store.get_node(u2_id) do
+        cond do
+          # --- Start of Logic for Placeholders ---
 
-        # TODO: Add cases to handle placeholder nodes co-inductively.
-        # Treat the placeholder as `any`.
-        match?({:ok, {:placeholder, _}}, {:ok, u1_details}) ->
-          # op(placeholder, u2) -> op(any, u2)
-          op_lambda.(:true_terminal, u2_details)
-          |> case do
-            :true_terminal -> Store.true_node_id()
-            :false_terminal -> Store.false_node_id()
-            # This happens if op(any, u2) = u2 (e.g., intersection)
-            _other -> u2_id
-          end
+          # Case 1: u2 is a placeholder. We must handle this based on u1.
+          match?({:placeholder, _}, u2_details) ->
+            case u1_details do
+              # op(true, placeholder) depends on the operation.
+              :true_terminal ->
+                case op_name do
+                  :sum -> Store.true_node_id()
+                  # intersect(any, p) = p
+                  :intersect -> u2_id
+                end
 
-        match?({:ok, {:placeholder, _}}, {:ok, u2_details}) ->
-          # op(u1, placeholder) -> op(u1, any)
-          op_lambda.(u1_details, :true_terminal)
-          |> case do
-            :true_terminal -> Store.true_node_id()
-            :false_terminal -> Store.false_node_id()
-            # This happens if op(u1, any) = u1 (e.g., intersection)
-            _other -> u1_id
-          end
+              # op(false, placeholder) also depends on the operation.
+              :false_terminal ->
+                case op_name do
+                  # sum(none, p) = p
+                  :sum -> u2_id
+                  :intersect -> Store.false_node_id()
+                end
 
-        u1_details == :true_terminal or u1_details == :false_terminal ->
-          {var2, y2, n2, d2} = u2_details
+              # op(node, placeholder) -> recursively apply op to children and placeholder.
+              {var1, y1, n1, d1} ->
+                Store.find_or_create_node(
+                  var1,
+                  apply(op_name, op_lambda, y1, u2_id),
+                  apply(op_name, op_lambda, n1, u2_id),
+                  apply(op_name, op_lambda, d1, u2_id)
+                )
+            end
 
-          Store.find_or_create_node(
-            var2,
-            apply(op_name, op_lambda, u1_id, y2),
-            apply(op_name, op_lambda, u1_id, n2),
-            apply(op_name, op_lambda, u1_id, d2)
-          )
+          # Case 2: Symmetric case where u1 is the placeholder.
+          match?({:placeholder, _}, u1_details) ->
+            case u2_details do
+              :true_terminal ->
+                case op_name do
+                  :sum -> Store.true_node_id()
+                  # intersect(p, any) = p
+                  :intersect -> u1_id
+                end
 
-        u2_details == :true_terminal or u2_details == :false_terminal ->
-          {var1, y1, n1, d1} = u1_details
+              :false_terminal ->
+                case op_name do
+                  # sum(p, none) = p
+                  :sum -> u1_id
+                  :intersect -> Store.false_node_id()
+                end
 
-          Store.find_or_create_node(
-            var1,
-            apply(op_name, op_lambda, y1, u2_id),
-            apply(op_name, op_lambda, n1, u2_id),
-            apply(op_name, op_lambda, d1, u2_id)
-          )
+              {var2, y2, n2, d2} ->
+                Store.find_or_create_node(
+                  var2,
+                  apply(op_name, op_lambda, u1_id, y2),
+                  apply(op_name, op_lambda, u1_id, n2),
+                  apply(op_name, op_lambda, u1_id, d2)
+                )
+            end
 
-        true ->
-          {var1, y1, n1, d1} = u1_details
-          {var2, y2, n2, d2} = u2_details
-          top_var = Enum.min([var1, var2])
+          # --- End of Placeholder Logic ---
+          # The rest of the function is the standard apply algorithm.
 
-          res_y =
-            apply(
-              op_name,
-              op_lambda,
-              if(var1 == top_var, do: y1, else: u1_id),
-              if(var2 == top_var, do: y2, else: u2_id)
+          (u1_details == :true_terminal or u1_details == :false_terminal) and
+              (u2_details == :true_terminal or u2_details == :false_terminal) ->
+            if op_lambda.(u1_details, u2_details) == :true_terminal,
+              do: Store.true_node_id(),
+              else: Store.false_node_id()
+
+          u1_details == :true_terminal or u1_details == :false_terminal ->
+            {var2, y2, n2, d2} = u2_details
+
+            Store.find_or_create_node(
+              var2,
+              apply(op_name, op_lambda, u1_id, y2),
+              apply(op_name, op_lambda, u1_id, n2),
+              apply(op_name, op_lambda, u1_id, d2)
             )
 
-          res_n =
-            apply(
-              op_name,
-              op_lambda,
-              if(var1 == top_var, do: n1, else: u1_id),
-              if(var2 == top_var, do: n2, else: u2_id)
+          u2_details == :true_terminal or u2_details == :false_terminal ->
+            {var1, y1, n1, d1} = u1_details
+
+            Store.find_or_create_node(
+              var1,
+              apply(op_name, op_lambda, y1, u2_id),
+              apply(op_name, op_lambda, n1, u2_id),
+              apply(op_name, op_lambda, d1, u2_id)
             )
 
-          res_d =
-            apply(
-              op_name,
-              op_lambda,
-              if(var1 == top_var, do: d1, else: u1_id),
-              if(var2 == top_var, do: d2, else: u2_id)
-            )
+          true ->
+            {var1, y1, n1, d1} = u1_details
+            {var2, y2, n2, d2} = u2_details
+            top_var = Enum.min([var1, var2])
 
-          Store.find_or_create_node(top_var, res_y, res_n, res_d)
+            res_y =
+              apply(
+                op_name,
+                op_lambda,
+                if(var1 == top_var, do: y1, else: u1_id),
+                if(var2 == top_var, do: y2, else: u2_id)
+              )
+
+            res_n =
+              apply(
+                op_name,
+                op_lambda,
+                if(var1 == top_var, do: n1, else: u1_id),
+                if(var2 == top_var, do: n2, else: u2_id)
+              )
+
+            res_d =
+              apply(
+                op_name,
+                op_lambda,
+                if(var1 == top_var, do: d1, else: u1_id),
+                if(var2 == top_var, do: d2, else: u2_id)
+              )
+
+            Store.find_or_create_node(top_var, res_y, res_n, res_d)
+        end
       end
     end
   end
@@ -1539,12 +1583,13 @@ defmodule Tdd.Algo do
   end
 
   defp do_simplify(tdd_id, sorted_assumptions, context) do
-    current_state = {tdd_id, sorted_assumptions}
-
-    if MapSet.member?(context, current_state) do
-      Store.true_node_id()
+    # The context now only tracks the node ID. If we see the same ID again,
+    # it's an unproductive loop, regardless of the path taken to get here.
+    if MapSet.member?(context, tdd_id) do
+      Store.false_node_id()
     else
-      new_context = MapSet.put(context, current_state)
+      # Add the current ID to the context for all subsequent recursive calls.
+      new_context = MapSet.put(context, tdd_id)
       assumptions = Map.new(sorted_assumptions)
 
       if Engine.check(assumptions) == :contradiction do
@@ -1557,8 +1602,13 @@ defmodule Tdd.Algo do
           {:ok, :false_terminal} ->
             Store.false_node_id()
 
+          {:ok, {:placeholder, _}} ->
+            # A placeholder should not exist in a fully formed graph being simplified.
+            # This indicates that the knot-tying in the compiler did not fully resolve
+            # the cycle. Encountering it means this path is unsatisfiable.
+            Store.false_node_id()
+
           {:ok, {var, y, n, d}} ->
-            # Dispatch to the handler for recursive variables.
             case var do
               {5, :c_head, constraint_id, _} ->
                 handle_recursive_subproblem(
@@ -1975,6 +2025,8 @@ defmodule Tdd.Compiler do
         id_to_cache =
           case normalized_spec do
             {:type_var, var_name} ->
+              Debug.log(Map.get(context, var_name), "{:type_var, var_name}")
+
               Map.get(context, var_name) ||
                 raise "Tdd.Compiler: Unbound type variable: #{inspect(var_name)}"
 
@@ -1989,7 +2041,6 @@ defmodule Tdd.Compiler do
 
               # "Tie the knot": substitute the placeholder with the ID of the body's root.
               # This correctly forms the cyclic TDD graph using the standard algorithm.
-              # The `substitute` function is designed for this and does not corrupt the store.
               final_id =
                 Algo.substitute(
                   body_id_with_placeholder,
@@ -1998,10 +2049,12 @@ defmodule Tdd.Compiler do
                 )
 
               # The resulting graph may have new simplification opportunities after the knot is tied.
+              # This call to simplify, with the corrected algorithm from Fix #1, is CRITICAL.
               Algo.simplify(final_id)
 
             other_spec ->
               raw_id = do_structural_compile(other_spec, context)
+              # Debug.build_graph_map(raw_id, "other spec id, before simplify")
               Algo.simplify(raw_id)
           end
 
@@ -2058,26 +2111,34 @@ defmodule Tdd.Compiler do
         Algo.negate(compile_normalized_spec(sub_spec, context))
 
       {:cons, head_spec, tail_spec} ->
-        id_list = compile_normalized_spec(:list, context)
-        id_is_empty = create_base_type_tdd(Variable.v_list_is_empty())
-        id_not_is_empty = Algo.negate(id_is_empty)
+        # --- NEW GUARD CLAUSE ---
+        # If the head or tail of a cons is known to be impossible (:none),
+        # then the entire cons expression is impossible to construct.
+        if head_spec == :none or tail_spec == :none do
+          Store.false_node_id()
+        else
+          # --- EXISTING LOGIC (now safely in the 'else' block) ---
+          id_list = compile_normalized_spec(:list, context)
+          id_is_empty = create_base_type_tdd(Variable.v_list_is_empty())
+          id_not_is_empty = Algo.negate(id_is_empty)
 
-        non_empty_list_id =
-          Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty)
+          non_empty_list_id =
+            Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty)
 
-        head_id = compile_normalized_spec(head_spec, context)
-        tail_id = compile_normalized_spec(tail_spec, context)
+          head_id = compile_normalized_spec(head_spec, context)
+          tail_id = compile_normalized_spec(tail_spec, context)
 
-        head_checker_var = Variable.v_list_head_pred(head_id)
-        head_checker_tdd = create_base_type_tdd(head_checker_var)
+          head_checker_var = Variable.v_list_head_pred(head_id)
+          head_checker_tdd = create_base_type_tdd(head_checker_var)
 
-        tail_checker_var = Variable.v_list_tail_pred(tail_id)
-        tail_checker_tdd = create_base_type_tdd(tail_checker_var)
+          tail_checker_var = Variable.v_list_tail_pred(tail_id)
+          tail_checker_tdd = create_base_type_tdd(tail_checker_var)
 
-        [non_empty_list_id, head_checker_tdd, tail_checker_tdd]
-        |> Enum.reduce(Store.true_node_id(), fn id, acc ->
-          Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
-        end)
+          [non_empty_list_id, head_checker_tdd, tail_checker_tdd]
+          |> Enum.reduce(Store.true_node_id(), fn id, acc ->
+            Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
+          end)
+        end
 
       {:tuple, elements_specs} ->
         size = length(elements_specs)
diff --git a/test/til_test.exs b/test/til_test.exs
index 3f4608a..7fb1575 100644
--- a/test/til_test.exs
+++ b/test/til_test.exs
@@ -32,8 +32,8 @@ defmodule TddSystemTest do
     quote do
       id1 = Compiler.spec_to_id(unquote(spec1))
       id2 = Compiler.spec_to_id(unquote(spec2))
-      Debug.build_graph_map(id1, "assert_equivalent_specs id1")
-      Debug.build_graph_map(id2, "assert_equivalent_specs id2")
+      # Debug.build_graph_map(id1, "assert_equivalent_specs id1")
+      # Debug.build_graph_map(id2, "assert_equivalent_specs id2")
       Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
       Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
       IO.inspect("equvalent specs? #{id1} #{id2}")
@@ -533,6 +533,9 @@ defmodule TddSystemTest do
       # list_of(integer & atom) is list_of(:none).
       # A list of :none can only be the empty list, as no element can ever exist.
       spec = {:list_of, {:intersect, [:integer, :atom]}}
+      Tdd.Store.init()
+      Debug.print_tdd_graph(Compiler.spec_to_id(spec))
+      Debug.print_tdd_graph(Compiler.spec_to_id({:literal, []}))
       assert_equivalent_specs(spec, {:literal, []})
     end
   end