diff --git a/ProofLibrary/ChaseSequence/Basic.lean b/ProofLibrary/ChaseSequence/Basic.lean
index 5ca8c6d..3e884d9 100644
--- a/ProofLibrary/ChaseSequence/Basic.lean
+++ b/ProofLibrary/ChaseSequence/Basic.lean
@@ -85,6 +85,7 @@ def not_exists_trigger_opt_fs (obs : ObsoletenessCondition sig) (rules : RuleSet
 def not_exists_trigger_list (obs : ObsoletenessCondition sig) (rules : RuleSet sig) (before : ChaseNode obs rules) (after : List (ChaseNode obs rules)) : Prop :=
   ¬(∃ trg : (RTrigger obs rules), trg.val.active before.fact) ∧ after = []
 
+@[ext]
 structure ChaseBranch (obs : ObsoletenessCondition sig) (kb : KnowledgeBase sig) where
   branch : PossiblyInfiniteList (ChaseNode obs kb.rules)
   database_first : branch.infinite_list 0 = some { fact := kb.db.toFactSet, origin := none, fact_contains_origin_result := by simp [Option.is_none_or] }
@@ -378,8 +379,8 @@ theorem chaseTreeSetIsSubsetOfResult (ct : ChaseTree obs kb) : ∀ node : List N
       unfold PossiblyInfiniteTree.branches_through at branch_through_node
       unfold InfiniteTreeSkeleton.branches_through at branch_through_node
       simp [Set.element] at branch_through_node
-      rw [branch_through_node.right ⟨node.length, by simp⟩]
-      simp
+      rcases branch_through_node with ⟨nodes, eq, eq2⟩
+      rw [eq node.length, eq2]
       rfl
 
     have branch_subs_result := chaseBranchSetIsSubsetOfResult branch node.length
diff --git a/ProofLibrary/ChaseSequence/Deterministic.lean b/ProofLibrary/ChaseSequence/Deterministic.lean
index 19a646b..37f4176 100644
--- a/ProofLibrary/ChaseSequence/Deterministic.lean
+++ b/ProofLibrary/ChaseSequence/Deterministic.lean
@@ -175,22 +175,25 @@ theorem ChaseTree.firstResult_is_in_result (ct : ChaseTree obs kb) : ct.firstRes
     unfold FiniteDegreeTree.branches
     unfold PossiblyInfiniteTree.branches
     unfold InfiniteTreeSkeleton.branches
+    unfold InfiniteTreeSkeleton.branches_through
     simp [firstBranch, Set.element]
     let nodes : InfiniteList Nat := fun _ => 0
     exists nodes
-    intro n
-    unfold FiniteDegreeTree.get
-    unfold PossiblyInfiniteTree.get
-    have : List.repeat 0 n = (nodes.take n).reverse := by
-      simp only [nodes]
-      induction n with
-      | zero => simp [List.repeat, InfiniteList.take]
-      | succ n ih =>
-        unfold List.repeat
-        unfold InfiniteList.take
-        simp
-        exact ih
-    rw [this]
+    constructor
+    . intro n
+      unfold FiniteDegreeTree.get
+      unfold PossiblyInfiniteTree.get
+      have : List.repeat 0 n = (nodes.take n).reverse := by
+        simp only [nodes]
+        induction n with
+        | zero => simp [List.repeat, InfiniteList.take]
+        | succ n ih =>
+          unfold List.repeat
+          unfold InfiniteList.take
+          simp
+          exact ih
+      rw [this]
+    . rfl
   . unfold ChaseBranch.result
     rfl
 
@@ -218,11 +221,11 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
           | some node =>
             have trg_ex := ct.triggers_exist (nodes.take n).reverse
             simp [Option.is_none_or]
-            have n_succ_in_ct := branch_in_ct (n+1)
+            have n_succ_in_ct := branch_in_ct.left (n+1)
             rw [eq] at n_succ_in_ct
             unfold FiniteDegreeTree.get at trg_ex
             unfold PossiblyInfiniteTree.get at trg_ex
-            rw [← branch_in_ct] at trg_ex
+            rw [← branch_in_ct.left] at trg_ex
             cases eq_prev : branch.branch.infinite_list n with
             | none =>
               have no_holes := branch.branch.no_holes (n+1) (by rw [eq]; simp) ⟨n, by simp⟩
@@ -260,7 +263,7 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
               | inr trg_ex =>
                 unfold not_exists_trigger_list at trg_ex
                 have contra := ct.tree.children_empty_means_all_following_none (nodes.take n).reverse trg_ex.right (nodes n)
-                specialize branch_in_ct (n+1)
+                have branch_in_ct := branch_in_ct.left (n+1)
                 unfold InfiniteList.take at branch_in_ct
                 simp at branch_in_ct
                 unfold FiniteDegreeTree.get at contra
@@ -310,7 +313,7 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
               have eq' := eq
               unfold FiniteDegreeTree.get at eq
               unfold PossiblyInfiniteTree.get at eq
-              rw [← branch_in_ct] at eq
+              rw [← branch_in_ct.left] at eq
               specialize this n
               rw [eq] at this; simp [Option.is_none_or] at this
               rw [this] at eq'
@@ -322,7 +325,7 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
                 cases trg_ex with | intro _ trg_ex => cases trg_ex.right with | intro _ trg_ex =>
                   unfold FiniteDegreeTree.get at h
                   unfold PossiblyInfiniteTree.get at h
-                  rw [← branch_in_ct] at h
+                  rw [← branch_in_ct.left] at h
                   rw [h] at trg_ex
                   contradiction
               | inr trg_ex =>
@@ -357,16 +360,16 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
             rw [eq] at this
             simp [Option.is_none_or] at this
             rw [← this]
-            unfold FiniteDegreeTree.get; unfold PossiblyInfiniteTree.get; rw [← branch_in_ct]; exact h
+            unfold FiniteDegreeTree.get; unfold PossiblyInfiniteTree.get; rw [← branch_in_ct.left]; exact h
         . intro h; cases h with | intro n h =>
           exists n
-          rw [branch_in_ct]
+          rw [branch_in_ct.left]
           cases eq : branch.branch.infinite_list n with
           | none =>
             rw [nodes_none_means_first_branch_none n (by
               unfold FiniteDegreeTree.get
               unfold PossiblyInfiniteTree.get
-              rw [← branch_in_ct]
+              rw [← branch_in_ct.left]
               exact eq
             )] at h
             simp [Option.is_some_and] at h
diff --git a/ProofLibrary/ChaseSequence/Termination.lean b/ProofLibrary/ChaseSequence/Termination.lean
index 0ffffbf..50c1bfb 100644
--- a/ProofLibrary/ChaseSequence/Termination.lean
+++ b/ProofLibrary/ChaseSequence/Termination.lean
@@ -197,5 +197,157 @@ section GeneralResults
 
   end ChaseBranch
 
+  namespace ChaseTree
+
+    theorem finitely_many_branch_of_terminates (ct : ChaseTree obs kb) : ct.terminates -> ct.branches.finite := by
+      unfold terminates
+      unfold ChaseBranch.terminates
+      intro each_b_term
+
+      have : ∀ b, b ∈ ct.tree.branches -> ∃ i, b.infinite_list i = none := by
+        intro b b_mem
+        rcases b_mem with ⟨nodes, b_mem, _⟩
+
+        -- It might seem like byContradiction is not needed but we need the contra hypothesis to show that cb is a proper chase branch
+        apply Classical.byContradiction
+        intro contra
+
+        let cb : ChaseBranch obs kb := {
+          branch := b
+          database_first := by rw [← ct.database_first]; rw [b_mem]; simp [InfiniteList.take]; rfl
+          triggers_exist := by
+            intro n
+            cases eq : b.infinite_list n with
+            | none => simp [Option.is_none_or]
+            | some node =>
+              simp [Option.is_none_or]
+              have trgs_ex := ct.triggers_exist (nodes.take n).reverse
+              unfold FiniteDegreeTree.get at trgs_ex
+              unfold PossiblyInfiniteTree.get at trgs_ex
+              rw [← b_mem, eq] at trgs_ex
+              simp [Option.is_none_or] at trgs_ex
+              cases trgs_ex with
+              | inr trgs_ex =>
+                unfold not_exists_trigger_list at trgs_ex
+                have all_none := ct.tree.children_empty_means_all_following_none _ trgs_ex.right
+                specialize all_none (nodes n)
+                apply False.elim
+                apply contra
+                exists (n+1)
+                rw [b_mem]
+                unfold InfiniteList.take
+                simp
+                exact all_none
+              | inl trgs_ex =>
+                apply Or.inl
+                unfold exists_trigger_list at trgs_ex
+                unfold exists_trigger_opt_fs
+                sorry
+          fairness := by sorry
+        }
+
+        apply contra
+        specialize each_b_term cb (by exists nodes)
+        exact each_b_term
+
+      -- Koenig's Lemma
+      have : ct.tree.branches.finite := by
+        apply ct.tree.branches_finite_of_each_finite
+        apply this
+
+      rcases this with ⟨l, l_nodup, l_eq⟩
+
+      let cb_for_b (b : PossiblyInfiniteList (ChaseNode obs kb.rules)) : Option (ChaseBranch obs kb) :=
+        match (Classical.propDecidable (∃ (cb : ChaseBranch obs kb), cb.branch = b)) with
+        | .isTrue p => some (Classical.choose p)
+        | .isFalse _ => none
+
+      have := Classical.typeDecidableEq (ChaseBranch obs kb)
+      let filtered := (l.filterMap (fun b => cb_for_b b)).eraseDupsKeepRight
+
+      exists filtered
+      constructor
+      . apply List.nodup_eraseDupsKeepRight
+      . intro e
+        unfold filtered
+        rw [List.mem_eraseDupsKeepRight_iff]
+        unfold branches
+        simp
+        constructor
+        . intro h
+          rcases h with ⟨b, b_mem, b_eq⟩
+          unfold cb_for_b at b_eq
+          split at b_eq
+          case h_1 _ p _ =>
+            have spec := Classical.choose_spec p
+            injection b_eq with b_eq
+            rw [← b_eq]
+            simp [Set.element]
+            rw [spec]
+            apply (l_eq b).mp
+            exact b_mem
+          case h_2 _ p _ =>
+            simp at b_eq
+        . intro h
+          exists e.branch
+          rw [l_eq]
+          constructor
+          . exact h
+          . unfold cb_for_b
+            split
+            case h_1 _ p _ =>
+              have spec := Classical.choose_spec p
+              simp
+              apply ChaseBranch.ext
+              exact spec
+            case h_2 _ p _ =>
+              apply False.elim
+              apply p
+              exists e
+
+    theorem result_finite_of_branches_finite (ct : ChaseTree obs kb) : ct.branches.finite -> ct.result.finite := by
+      intro bs_finite
+      unfold Set.finite at bs_finite
+      rcases bs_finite with ⟨l, _, iff⟩
+      have : DecidableEq (FactSet sig) := Classical.typeDecidableEq (FactSet sig)
+      exists (l.map ChaseBranch.result).eraseDupsKeepRight
+      constructor
+      . apply List.nodup_eraseDupsKeepRight
+      . intro fs
+        rw [List.mem_eraseDupsKeepRight_iff]
+        simp
+        constructor
+        . intro h
+          rcases h with ⟨b, mem, eq⟩
+          exists b
+          constructor
+          . rw [← iff]; exact mem
+          . exact eq
+        . intro h
+          rcases h with ⟨b, mem, eq⟩
+          exists b
+          constructor
+          . rw [iff]; exact mem
+          . exact eq
+
+    theorem terminates_iff_result_finite (ct : ChaseTree obs kb) : ct.terminates ↔ ∀ fs, fs ∈ ct.result -> fs.finite := by
+      unfold terminates
+      unfold result
+      constructor
+      . intro each_b_term
+        intro res res_mem
+        rcases res_mem with ⟨b, mem, eq⟩
+        rw [← eq]
+        rw [← ChaseBranch.terminates_iff_result_finite]
+        apply each_b_term
+        exact mem
+      . intro each_b_term
+        intro b mem
+        rw [ChaseBranch.terminates_iff_result_finite]
+        apply each_b_term
+        exists b
+
+  end ChaseTree
+
 end GeneralResults
 
diff --git a/ProofLibrary/ChaseSequence/Universality.lean b/ProofLibrary/ChaseSequence/Universality.lean
index d55fbdd..8867274 100644
--- a/ProofLibrary/ChaseSequence/Universality.lean
+++ b/ProofLibrary/ChaseSequence/Universality.lean
@@ -868,15 +868,18 @@ theorem chaseTreeResultIsUniversal (ct : ChaseTree obs kb) : ∀ (m : FactSet si
     unfold FiniteDegreeTree.branches
     unfold PossiblyInfiniteTree.branches
     unfold InfiniteTreeSkeleton.branches
+    unfold InfiniteTreeSkeleton.branches_through
     unfold Set.element
     simp
     exists indices
-    intro n
-    simp only [path]
-    rw [indices_aux_result]
-    unfold FiniteDegreeTree.get
-    unfold PossiblyInfiniteTree.get
-    rfl
+    constructor
+    . intro n
+      simp only [path]
+      rw [indices_aux_result]
+      unfold FiniteDegreeTree.get
+      unfold PossiblyInfiniteTree.get
+      rfl
+    . rfl
   . constructor
     . intro gt
       split
diff --git a/ProofLibrary/PossiblyInfiniteList.lean b/ProofLibrary/PossiblyInfiniteList.lean
index e4b2f57..68fe7e2 100644
--- a/ProofLibrary/PossiblyInfiniteList.lean
+++ b/ProofLibrary/PossiblyInfiniteList.lean
@@ -7,6 +7,9 @@ namespace InfiniteList
   | 0 => []
   | n+1 => (l.take n) ++ [l n]
 
+  theorem length_take (l : InfiniteList α) (n : Nat) : (l.take n).length = n := by
+    induction n ; simp [take] ; simpa [take]
+
   def skip (l : InfiniteList α) (m : Nat) : InfiniteList α := fun n => l (n + m)
 
   theorem skip_zero_eq (l : InfiniteList α) : l.skip 0 = l := by unfold skip; simp only [Nat.add_zero]
@@ -39,6 +42,30 @@ namespace InfiniteList
         have : m = k := by cases Nat.lt_or_eq_of_le (Nat.le_of_lt_succ m.isLt); contradiction; assumption
         rw [this]
         simp [take]
+
+  theorem take_after_take (l : InfiniteList α) (n m : Nat) : (l.take n).take m = l.take (n.min m) := by
+    induction n with
+    | zero => simp [take]
+    | succ n ih =>
+      simp [take]
+      rw [List.take_append_eq_append_take]
+      rw [ih]
+      rw [length_take]
+      cases Decidable.em (n ≤ m) with
+      | inl le =>
+        simp [Nat.min_eq_left le]
+        cases Nat.eq_or_lt_of_le le with
+        | inl eq =>
+          rw [eq]
+          simp
+        | inr lt =>
+          simp [Nat.min_eq_left (Nat.succ_le_of_lt lt)]
+          conv => right; unfold InfiniteList.take
+          rw [List.take_of_length_le (by apply Nat.le_sub_of_add_le; rw [Nat.add_comm, List.length_singleton]; apply Nat.succ_le_of_lt; exact lt)]
+      | inr lt =>
+        simp at lt
+        simp [Nat.min_eq_right (Nat.le_of_lt lt), Nat.min_eq_right (Nat.le_succ_of_le (Nat.le_of_lt lt))]
+        apply Nat.sub_eq_zero_of_le (Nat.le_of_lt lt)
 end InfiniteList
 
 @[ext]
diff --git a/ProofLibrary/PossiblyInfiniteTree.lean b/ProofLibrary/PossiblyInfiniteTree.lean
index abad770..89936ed 100644
--- a/ProofLibrary/PossiblyInfiniteTree.lean
+++ b/ProofLibrary/PossiblyInfiniteTree.lean
@@ -8,13 +8,43 @@ import ProofLibrary.PossiblyInfiniteList
 def InfiniteTreeSkeleton (α : Type u) := (List Nat) -> α
 
 namespace InfiniteTreeSkeleton
-  def children (tree : InfiniteTreeSkeleton α) (node : List Nat) : InfiniteList α := fun n => tree (n :: node)
 
-  def branches (tree : InfiniteTreeSkeleton α) : Set (InfiniteList α) := fun branch =>
-    ∃ nodes : InfiniteList Nat, ∀ n : Nat, branch n = tree (nodes.take n).reverse
+  def children (tree : InfiniteTreeSkeleton α) (node : List Nat) : InfiniteList α := fun n => tree (n :: node)
 
   def branches_through (tree : InfiniteTreeSkeleton α) (node : List Nat) : Set (InfiniteList α) := fun branch =>
-    branch ∈ tree.branches ∧ ∀ (i : Fin (node.length + 1)), branch i = tree (node.drop (node.length-i))
+    ∃ nodes : InfiniteList Nat, (∀ n : Nat, branch n = tree (nodes.take n).reverse) ∧ (nodes.take node.length).reverse = node
+
+  def branches (tree : InfiniteTreeSkeleton α) : Set (InfiniteList α) := tree.branches_through []
+
+  theorem branches_through_eq_union_children (tree : InfiniteTreeSkeleton α) (node : List Nat) : tree.branches_through node = fun b => ∃ (i : Nat), b ∈ tree.branches_through (i :: node) := by
+    unfold branches_through
+    apply funext
+    simp
+    intro b
+    constructor
+    . intro ⟨nodes, h⟩
+      exists nodes node.length
+      simp [Set.element]
+      exists nodes
+      constructor
+      . exact h.left
+      . unfold InfiniteList.take
+        simp
+        rw [← List.reverse_eq_iff]
+        exact h.right
+    . intro h
+      rcases h with ⟨i, nodes, h⟩
+      exists nodes
+      constructor
+      . exact h.left
+      . have hr := h.right
+        unfold InfiniteList.take at hr
+        rw [← List.reverse_inj] at hr
+        rw [List.reverse_append] at hr
+        rw [List.reverse_append] at hr
+        simp at hr
+        exact hr.right
+
 end InfiniteTreeSkeleton
 
 structure PossiblyInfiniteTree (α : Type u) where
@@ -82,11 +112,25 @@ namespace PossiblyInfiniteTree
     unfold InfiniteTreeSkeleton.children
     simp
 
+  def branches_through (tree : PossiblyInfiniteTree α) (node : List Nat) : Set (PossiblyInfiniteList α) := fun pil =>
+    pil.infinite_list ∈ tree.infinite_tree.branches_through node
+
   def branches (tree : PossiblyInfiniteTree α) : Set (PossiblyInfiniteList α) := fun pil =>
     pil.infinite_list ∈ tree.infinite_tree.branches
 
-  def branches_through (tree : PossiblyInfiniteTree α) (node : List Nat) : Set (PossiblyInfiniteList α) := fun pil =>
-    pil.infinite_list ∈ tree.infinite_tree.branches_through node
+  theorem branches_through_eq_union_children (tree : PossiblyInfiniteTree α) (node : List Nat) : tree.branches_through node = fun b => ∃ (i : Nat), b ∈ tree.branches_through (i :: node) := by
+    unfold branches_through
+    apply funext
+    simp
+    intro pil
+    rw [tree.infinite_tree.branches_through_eq_union_children]
+    constructor
+    . intro h
+      rcases h with ⟨i, h⟩
+      exists i
+    . intro h
+      rcases h with ⟨i, h⟩
+      exists i
 
   def leaves (tree : PossiblyInfiniteTree α) : Set α := fun a => ∃ node : List Nat, tree.get node = some a ∧ tree.children node = PossiblyInfiniteList.empty
 end PossiblyInfiniteTree
@@ -389,10 +433,377 @@ namespace FiniteDegreeTree
     rw [PossiblyInfiniteList.get_fromList_eq_list_getElem]
     apply getElem_children_eq_getElem_tree_children
 
+  def branches_through (tree : FiniteDegreeTree α) (node : List Nat) : Set (PossiblyInfiniteList α) := tree.tree.branches_through node
+
   def branches (tree : FiniteDegreeTree α) : Set (PossiblyInfiniteList α) := tree.tree.branches
 
-  def branches_through (tree : FiniteDegreeTree α) (node : List Nat) : Set (PossiblyInfiniteList α) := tree.tree.branches_through node
+  theorem branches_through_eq_union_children (tree : FiniteDegreeTree α) (node : List Nat) : tree.branches_through node = fun b => ∃ (i : Nat), b ∈ tree.branches_through (i :: node) := by
+    unfold branches_through
+    rw [tree.tree.branches_through_eq_union_children]
 
   def leaves (tree : FiniteDegreeTree α) : Set α := tree.tree.leaves
+
+  theorem branches_through_finite_of_none (tree : FiniteDegreeTree α) (node : List Nat) : tree.get node = none -> (tree.branches_through node).finite := by
+    intro is_none
+    let branch_for_node : PossiblyInfiniteList α := ⟨fun n => if n ≤ node.length then tree.get (node.drop (node.length - n)) else none, by
+      intro n not_none
+      cases Decidable.em (n ≤ node.length) with
+      | inr lt => simp [lt] at not_none
+      | inl le =>
+        simp [le] at not_none
+        intro m
+        have m_le : m ≤ node.length := by apply Nat.le_trans; apply Nat.le_of_lt m.isLt; exact le
+        simp [m_le]
+        have no_orphans := tree.tree.no_orphans (node.drop (node.length - n)) not_none ⟨(node.drop (node.length - m)), by
+          exists (node.drop (node.length - n)).take (n - m)
+          rw [List.take_drop]
+          have : node.length - n + (n - m.val) = node.length - m.val := by
+            rw [← Nat.add_sub_assoc (by apply Nat.le_of_lt; exact m.isLt)]
+            rw [← Nat.sub_add_comm le]
+            simp
+          rw [this]
+          rw [← List.drop_append_of_le_length (by rw [List.length_take_of_le (by simp), Nat.sub_le_sub_iff_left m_le]; apply Nat.le_of_lt; exact m.isLt)]
+          simp
+        ⟩
+        exact no_orphans
+    ⟩
+    exists [branch_for_node]
+    constructor
+    . simp
+    . intro e
+      constructor
+      . intro h
+        simp at h
+        rw [h]
+        let nodes : InfiniteList Nat := fun n => if lt : n < node.length then node[node.length - (n+1)] else (tree.children node).length
+        have : ∀ n, n ≤ node.length -> (nodes.take n).reverse = node.drop (node.length - n) := by
+          intro n
+          induction n with
+          | zero => simp [InfiniteList.take]
+          | succ n ih =>
+            intro le
+            unfold InfiniteList.take
+            simp
+            rw [ih (by apply Nat.le_of_succ_le le)]
+            unfold nodes
+            have lt : n < node.length := by apply Nat.lt_of_succ_le le
+            simp [lt]
+            conv => right; rw [List.drop_eq_getElem_cons (by apply Nat.sub_lt_self; simp; exact le)]
+            have : node.length - (n + 1) + 1 = node.length - n := by omega
+            rw [this]
+        exists nodes
+        constructor
+        . intro n
+          cases Decidable.em (n ≤ node.length) with
+          | inl le =>
+            rw [this n le]
+            simp [le]
+            rfl
+          | inr lt =>
+            simp [lt]
+            have no_orphans := tree.tree.no_orphans (nodes.take n).reverse
+            apply Eq.symm
+            apply Option.decidable_eq_none.byContradiction
+            intro contra
+            specialize no_orphans contra ⟨node, by
+              exists ((nodes.skip (node.length)).take (n - node.length)).reverse
+              have : node = (nodes.take (node.length)).reverse := by
+                rw [this node.length]
+                . simp
+                . simp
+              conv => left; right; rw [this]
+              rw [← List.reverse_append]
+              rw [InfiniteList.combine_skip_take nodes n ⟨node.length, by apply Nat.lt_of_not_le; exact lt⟩]
+            ⟩
+            apply no_orphans
+            exact is_none
+        . rw [this]
+          . simp
+          . simp
+      . intro h
+        rcases h with ⟨nodes, h⟩
+        simp
+        rw [PossiblyInfiniteList.eq_iff_same_on_all_indices]
+        intro n
+        rw [h.left]
+        unfold branch_for_node
+        simp
+        cases Decidable.em (n ≤ node.length) with
+        | inl le =>
+          simp [le]
+          have : (nodes.take n).reverse = node.drop (node.length - n) := by
+            conv => right; right; rw [← h.right]
+            rw [List.drop_reverse]
+            rw [InfiniteList.length_take]
+            rw [InfiniteList.take_after_take]
+            rw [Nat.sub_sub_self le]
+            simp [Nat.min_eq_right le]
+          rw [this]
+          rfl
+        | inr lt =>
+          simp [lt]
+
+          have no_orphans := tree.tree.no_orphans (nodes.take n).reverse
+          apply Option.decidable_eq_none.byContradiction
+          intro contra
+          specialize no_orphans contra ⟨node, by
+            exists ((nodes.skip (node.length)).take (n - node.length)).reverse
+            conv => left; right; rw [← h.right]
+            rw [← List.reverse_append]
+            rw [InfiniteList.combine_skip_take nodes n ⟨node.length, by apply Nat.lt_of_not_le; exact lt⟩]
+          ⟩
+          apply no_orphans
+          exact is_none
+
+  theorem branches_through_finite_of_branches_through_children_finite (tree : FiniteDegreeTree α) (node : List Nat) : (∀ i, (tree.branches_through (i :: node)).finite) -> (tree.branches_through node).finite := by
+    intro h
+    have dec := Classical.typeDecidableEq (PossiblyInfiniteList α)
+    let branch_for_node : PossiblyInfiniteList α := ⟨fun n => if n ≤ node.length then tree.get (node.drop (node.length - n)) else none, by
+      intro n not_none
+      cases Decidable.em (n ≤ node.length) with
+      | inr lt => simp [lt] at not_none
+      | inl le =>
+        simp [le] at not_none
+        intro m
+        have m_le : m ≤ node.length := by apply Nat.le_trans; apply Nat.le_of_lt m.isLt; exact le
+        simp [m_le]
+        have no_orphans := tree.tree.no_orphans (node.drop (node.length - n)) not_none ⟨(node.drop (node.length - m)), by
+          exists (node.drop (node.length - n)).take (n - m)
+          rw [List.take_drop]
+          have : node.length - n + (n - m.val) = node.length - m.val := by
+            rw [← Nat.add_sub_assoc (by apply Nat.le_of_lt; exact m.isLt)]
+            rw [← Nat.sub_add_comm le]
+            simp
+          rw [this]
+          rw [← List.drop_append_of_le_length (by rw [List.length_take_of_le (by simp), Nat.sub_le_sub_iff_left m_le]; apply Nat.le_of_lt; exact m.isLt)]
+          simp
+        ⟩
+        exact no_orphans
+    ⟩
+    let branches_for_i (i : Nat) := Classical.choose (h i)
+    let target_list : List (PossiblyInfiniteList α) := (branch_for_node :: ((tree.children node).enum_with_lt.map (fun (i, _) => branches_for_i i.val)).flatten).eraseDupsKeepRight
+    exists target_list
+    constructor
+    . apply List.nodup_eraseDupsKeepRight
+    . intro branch
+      unfold target_list
+      rw [List.mem_eraseDupsKeepRight_iff]
+      simp
+      constructor
+      . intro pre
+        cases pre with
+        | inl eq =>
+          let nodes : InfiniteList Nat := fun n => if lt : n < node.length then node[node.length - (n+1)] else (tree.children node).length
+          have : ∀ n, n ≤ node.length -> (nodes.take n).reverse = node.drop (node.length - n) := by
+            intro n
+            induction n with
+            | zero => simp [InfiniteList.take]
+            | succ n ih =>
+              intro le
+              unfold InfiniteList.take
+              simp
+              rw [ih (by apply Nat.le_of_succ_le le)]
+              unfold nodes
+              have lt : n < node.length := by apply Nat.lt_of_succ_le le
+              simp [lt]
+              conv => right; rw [List.drop_eq_getElem_cons (by apply Nat.sub_lt_self; simp; exact le)]
+              have : node.length - (n + 1) + 1 = node.length - n := by omega
+              rw [this]
+          exists nodes
+          constructor
+          . rw [eq]
+            intro n
+            cases Decidable.em (n ≤ node.length) with
+            | inl le =>
+              rw [this n le]
+              simp [le]
+              rfl
+            | inr lt =>
+              simp [lt]
+              have : tree.tree.infinite_tree (nodes.take (node.length + 1)).reverse = none := by
+                have child_none : (tree.children node)[nodes node.length]? = none := by
+                  apply List.getElem?_eq_none
+                  unfold nodes
+                  simp
+                rw [getElem_children_eq_getElem_tree_children, PossiblyInfiniteTree.getElem_children_eq_get_tree] at child_none
+                unfold PossiblyInfiniteTree.get at child_none
+                unfold InfiniteList.take
+                simp
+                rw [this]
+                . simp
+                  exact child_none
+                . simp
+              have le : node.length + 1 ≤ n := by apply Nat.succ_le_of_lt; apply Nat.lt_of_not_ge; exact lt
+              cases Nat.eq_or_lt_of_le le with
+              | inl eq => rw [← eq, this]
+              | inr lt =>
+                have no_orphans := tree.tree.no_orphans (nodes.take n).reverse
+                apply Eq.symm
+                apply Option.decidable_eq_none.byContradiction
+                intro contra
+                specialize no_orphans contra ⟨(nodes.take (node.length + 1)).reverse, by
+                  exists ((nodes.skip (node.length + 1)).take (n - (node.length + 1))).reverse
+                  rw [← List.reverse_append]
+                  rw [InfiniteList.combine_skip_take nodes n ⟨node.length + 1, lt⟩]
+                ⟩
+                apply no_orphans
+                exact this
+          . rw [this]
+            . simp
+            . simp
+        | inr pre =>
+          rcases pre with ⟨branches, ex_i, branch_mem⟩
+          rcases ex_i with ⟨i, _, eq⟩
+          rw [branches_through_eq_union_children]
+          exists i.val
+          have spec := Classical.choose_spec (h i.val)
+          rw [← spec.right]
+          unfold branches_for_i at eq
+          rw [eq]
+          exact branch_mem
+      . intro pre
+        rw [branches_through_eq_union_children] at pre
+        rcases pre with ⟨i, pre⟩
+        cases Decidable.em (i < (tree.children node).length) with
+        | inl lt =>
+          apply Or.inr
+          exists branches_for_i i
+          constructor
+          . let i_fin : Fin (tree.children node).length := ⟨i, lt⟩
+            exists i_fin
+            constructor
+            . exists (tree.children node)[i_fin]
+              rw [List.mem_enum_with_lt_iff_mem_enum]
+              rw [List.mem_enum_iff_getElem?]
+              simp
+            . rfl
+          . have spec := Classical.choose_spec (h i)
+            unfold branches_for_i
+            rw [spec.right]
+            exact pre
+        | inr not_lt =>
+          apply Or.inl
+          rcases pre with ⟨nodes, pre⟩
+          unfold branch_for_node
+          rw [PossiblyInfiniteList.eq_iff_same_on_all_indices]
+          intro n
+          rw [pre.left n]
+          have pre_r := pre.right
+          simp [InfiniteList.take] at pre_r
+          simp
+          cases Decidable.em (n ≤ node.length) with
+          | inl le =>
+            simp [le]
+            have : (nodes.take n).reverse = node.drop (node.length - n) := by
+              conv => right; right; rw [← pre_r.right]
+              rw [List.drop_reverse]
+              rw [InfiniteList.length_take]
+              rw [InfiniteList.take_after_take]
+              rw [Nat.sub_sub_self le]
+              simp [Nat.min_eq_right le]
+            rw [this]
+            rfl
+          | inr lt =>
+            simp [lt]
+            have : tree.tree.infinite_tree (nodes.take (node.length + 1)).reverse = none := by
+              have : (tree.children node)[nodes node.length]? = none := by
+                apply List.getElem?_eq_none
+                rw [pre_r.left]
+                apply Nat.le_of_not_gt
+                exact not_lt
+              rw [getElem_children_eq_getElem_tree_children, PossiblyInfiniteTree.getElem_children_eq_get_tree] at this
+              unfold PossiblyInfiniteTree.get at this
+              unfold InfiniteList.take
+              simp
+              rw [pre_r.right]
+              exact this
+            have le : node.length + 1 ≤ n := by apply Nat.succ_le_of_lt; apply Nat.lt_of_not_ge; exact lt
+            cases Nat.eq_or_lt_of_le le with
+            | inl eq => rw [← eq]; exact this
+            | inr lt =>
+              have no_orphans := tree.tree.no_orphans (nodes.take n).reverse
+              apply Option.decidable_eq_none.byContradiction
+              intro contra
+              specialize no_orphans contra ⟨(nodes.take (node.length + 1)).reverse, by
+                exists ((nodes.skip (node.length + 1)).take (n - (node.length + 1))).reverse
+                rw [← List.reverse_append]
+                rw [InfiniteList.combine_skip_take nodes n ⟨node.length + 1, lt⟩]
+              ⟩
+              apply no_orphans
+              exact this
+
+  noncomputable def infinite_branching_node_for_depth_of_branches_infinite (tree : FiniteDegreeTree α) (not_finite : ¬ tree.branches.finite) : (depth : Nat) -> { node : List Nat // node.length = depth ∧ ¬ (tree.branches_through node).finite }
+  | .zero => ⟨[], by constructor; rfl; exact not_finite⟩
+  | .succ depth =>
+    let prev_res := infinite_branching_node_for_depth_of_branches_infinite tree not_finite depth
+    let prev_node := prev_res.val
+    let length_eq := prev_res.property.left
+    let not_finite := prev_res.property.right
+    have : ¬ ∀ i, (tree.branches_through (i :: prev_node)).finite := by
+      intro contra
+      apply not_finite
+      apply branches_through_finite_of_branches_through_children_finite
+      exact contra
+    have : ∃ i, ¬ (tree.branches_through (i :: prev_node)).finite := by simp at this; exact this
+    let i := Classical.choose this
+    let i_spec := Classical.choose_spec this
+
+    ⟨i :: prev_node, by
+      constructor
+      . simp; exact length_eq
+      . exact i_spec
+    ⟩
+
+  theorem infinite_branching_node_extends_previous (tree : FiniteDegreeTree α) (not_finite : ¬ tree.branches.finite) (depth : Nat) : (infinite_branching_node_for_depth_of_branches_infinite tree not_finite depth.succ).val = (infinite_branching_node_for_depth_of_branches_infinite tree not_finite depth.succ).val.head (by simp [infinite_branching_node_for_depth_of_branches_infinite]) :: (infinite_branching_node_for_depth_of_branches_infinite tree not_finite depth).val := by
+    simp [infinite_branching_node_for_depth_of_branches_infinite]
+
+  theorem branches_finite_of_each_finite (tree : FiniteDegreeTree α) : (∀ branch, branch ∈ tree.branches -> ∃ i, branch.infinite_list i = none) -> tree.branches.finite := by
+    intro h
+
+    apply Classical.byContradiction
+    intro contra
+    simp at contra
+
+    have : ∃ (nodes : InfiniteList Nat), ∀ (i : Nat), ¬ (tree.branches_through (nodes.take i).reverse).finite := by
+      let nodes : InfiniteList Nat := fun n => (infinite_branching_node_for_depth_of_branches_infinite tree contra n.succ).val.head (by
+        simp [infinite_branching_node_for_depth_of_branches_infinite]
+      )
+      have : ∀ i, (nodes.take i).reverse = (infinite_branching_node_for_depth_of_branches_infinite tree contra i).val := by
+        intro i
+        induction i with
+        | zero => simp [InfiniteList.take, infinite_branching_node_for_depth_of_branches_infinite]
+        | succ i ih =>
+          unfold InfiniteList.take
+          unfold nodes
+          simp
+          rw [ih]
+          conv => right; rw [infinite_branching_node_extends_previous]
+      exists nodes
+      intro i
+      rw [this]
+      have prop := (infinite_branching_node_for_depth_of_branches_infinite tree contra i).property
+      exact prop.right
+
+    rcases this with ⟨nodes, all_infinite⟩
+
+    let branch : PossiblyInfiniteList α := ⟨fun n => tree.get (nodes.take n).reverse, by
+      intro n not_none m contra
+      apply all_infinite m.val
+      apply branches_through_finite_of_none
+      exact contra
+    ⟩
+
+    specialize h branch (by
+      exists nodes
+      constructor
+      . intro n
+        rfl
+      . rfl
+    )
+
+    rcases h with ⟨i, hi⟩
+    apply all_infinite i
+    apply branches_through_finite_of_none
+    exact hi
 end FiniteDegreeTree