[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f1 => f1
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: 5 => 5
[Meta.Tactic.simp.ground] ✅️ seval: f1 [1, 2, 3] 5 => [6, 7, 8]
  [Meta.Tactic.simp.ground] unfolded, f1 [1, 2, 3] 5 => (1 + 5) :: f1 [2, 3] 5
  [Meta.Tactic.simp.ground] unfolded, f1 [2, 3] 5 => (2 + 5) :: f1 [3] 5
  [Meta.Tactic.simp.ground] unfolded, f1 [3] 5 => (3 + 5) :: f1 [] 5
  [Meta.Tactic.simp.ground] unfolded, f1 [] 5 => []
[Meta.Tactic.simp.ground] ✅️ seval: 6 => 6
[Meta.Tactic.simp.ground] ✅️ seval: 7 => 7
[Meta.Tactic.simp.ground] ✅️ seval: 8 => 8
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [7, 8] => [7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [6, 7, 8] => [6, 7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f2 => f2
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: 10 => 10
[Meta.Tactic.simp.ground] ✅️ seval: @Neg.neg => @Neg.neg
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 8 => 8
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [-2, 8] => [-2, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [10, -2, 8] => [10, -2, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 10, -2, 8] => [1, 10, -2, 8]
[Meta.Tactic.simp.ground] ✅️ seval: 5 => 5
[Meta.Tactic.simp.ground] ✅️ seval: f2 [1, 10, -2, 8] (-5) => [-3, 15, -9, 11]
  [Meta.Tactic.simp.ground] unfolded, f2 [1, 10, -2, 8] (-5) => add2 1 (-5) :: f2 [10, -2, 8] (-5)
  [Meta.Tactic.simp.ground] unfolded, add2 1 (-5) => 1 + 1 + -5
  [Meta.Tactic.simp.ground] unfolded, f2 [10, -2, 8] (-5) => add2 10 (-5) :: f2 [-2, 8] (-5)
  [Meta.Tactic.simp.ground] unfolded, add2 10 (-5) => 10 + 10 + -5
  [Meta.Tactic.simp.ground] unfolded, f2 [-2, 8] (-5) => add2 (-2) (-5) :: f2 [8] (-5)
  [Meta.Tactic.simp.ground] unfolded, add2 (-2) (-5) => -2 + -2 + -5
  [Meta.Tactic.simp.ground] unfolded, f2 [8] (-5) => add2 8 (-5) :: f2 [] (-5)
  [Meta.Tactic.simp.ground] unfolded, add2 8 (-5) => 8 + 8 + -5
  [Meta.Tactic.simp.ground] unfolded, f2 [] (-5) => []
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: 15 => 15
[Meta.Tactic.simp.ground] ✅️ seval: 9 => 9
[Meta.Tactic.simp.ground] ✅️ seval: 11 => 11
[Meta.Tactic.simp.ground] ✅️ seval: [11] => [11]
[Meta.Tactic.simp.ground] ✅️ seval: [-9, 11] => [-9, 11]
[Meta.Tactic.simp.ground] ✅️ seval: [15, -9, 11] => [15, -9, 11]
[Meta.Tactic.simp.ground] ✅️ seval: [-3, 15, -9, 11] => [-3, 15, -9, 11]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f3 => f3
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: 5 => 5
[Meta.Tactic.simp.ground] ✅️ seval: f3 [1, 2, 3] 5 => [6, 7, 8]
  [Meta.Tactic.simp.ground] unfolded, f3 [1, 2, 3] 5 => (1 + 5) :: f3 [2, 3] 5
  [Meta.Tactic.simp.ground] unfolded, f3 [2, 3] 5 => (2 + 5) :: f3 [3] 5
  [Meta.Tactic.simp.ground] unfolded, f3 [3] 5 => (3 + 5) :: f3 [] 5
  [Meta.Tactic.simp.ground] unfolded, f3 [] 5 => []
[Meta.Tactic.simp.ground] ✅️ seval: 6 => 6
[Meta.Tactic.simp.ground] ✅️ seval: 7 => 7
[Meta.Tactic.simp.ground] ✅️ seval: 8 => 8
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [7, 8] => [7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [6, 7, 8] => [6, 7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f4 => f4
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: f4 [1, 2, 3] 5 => [6, 7, 8]
  [Meta.Tactic.simp.ground] unfolded, f4 [1, 2, 3] 5 => (1 + 5) :: f4 [2, 3] 5
  [Meta.Tactic.simp.ground] unfolded, f4 [2, 3] 5 => (2 + 5) :: f4 [3] 5
  [Meta.Tactic.simp.ground] unfolded, f4 [3] 5 => (3 + 5) :: f4 [] 5
  [Meta.Tactic.simp.ground] unfolded, f4 [] 5 => []
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [7, 8] => [7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [6, 7, 8] => [6, 7, 8]
List.instAppend.{u} {α : Type u} : Append (List α)
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: @List.reverse => @List.reverse
[Meta.Tactic.simp.ground] ✅️ seval: @List.map => @List.map
[Meta.Tactic.simp.ground] ✅️ seval: @HAdd.hAdd => @HAdd.hAdd
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [4] => [4]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 4] => [3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3, 4] => [2, 3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: @HAppend.hAppend => @HAppend.hAppend
[Meta.Tactic.simp.ground] ✅️ seval: 4 => 4
[Meta.Tactic.simp.ground] ✅️ seval: [4] => [4]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 4] => [3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3] => [4, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [2] => [2]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 2] => [3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3, 2] => [4, 3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 2] => [3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3, 2] => [4, 3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: @rev => @rev
[Meta.Tactic.simp.ground] ✅️ seval: @List.map => @List.map
[Meta.Tactic.simp.ground] ✅️ seval: @HAdd.hAdd => @HAdd.hAdd
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [4] => [4]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 4] => [3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3, 4] => [2, 3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: rev [2, 3, 4] => [4, 3, 2]
  [Meta.Tactic.simp.ground] unfolded, rev [2, 3, 4] => rev [3, 4] ++ [2]
  [Meta.Tactic.simp.ground] unfolded, rev [3, 4] => rev [4] ++ [3]
  [Meta.Tactic.simp.ground] unfolded, rev [4] => rev [] ++ [4]
  [Meta.Tactic.simp.ground] unfolded, rev [] => []
  [Meta.Tactic.simp.ground] unfolded, [] ++ [4] => instHAppendOfAppend.1 [] [4]
  [Meta.Tactic.simp.ground] unfolded, instHAppendOfAppend => { hAppend := fun a b => Append.append a b }
  [Meta.Tactic.simp.ground] unfolded, Append.append [] [4] => List.instAppend.1 [] [4]
  [Meta.Tactic.simp.ground] unfolded, List.instAppend => { append := List.append }
  [Meta.Tactic.simp.ground] unfolded, [].append [4] => [4]
  [Meta.Tactic.simp.ground] unfolded, [4] ++ [3] => instHAppendOfAppend.1 [4] [3]
  [Meta.Tactic.simp.ground] unfolded, Append.append [4] [3] => List.instAppend.1 [4] [3]
  [Meta.Tactic.simp.ground] unfolded, [4].append [3] => 4 :: [].append [3]
  [Meta.Tactic.simp.ground] unfolded, [].append [3] => [3]
  [Meta.Tactic.simp.ground] unfolded, [4, 3] ++ [2] => instHAppendOfAppend.1 [4, 3] [2]
  [Meta.Tactic.simp.ground] unfolded, Append.append [4, 3] [2] => List.instAppend.1 [4, 3] [2]
  [Meta.Tactic.simp.ground] unfolded, [4, 3].append [2] => 4 :: [3].append [2]
  [Meta.Tactic.simp.ground] unfolded, [3].append [2] => 3 :: [].append [2]
  [Meta.Tactic.simp.ground] unfolded, [].append [2] => [2]
[Meta.Tactic.simp.ground] ✅️ seval: 4 => 4
[Meta.Tactic.simp.ground] ✅️ seval: [2] => [2]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 2] => [3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3, 2] => [4, 3, 2]