∀ (α α' : Type u_1),
  α = α' →
    ∀ (inst : DecidableEq α) (inst' : DecidableEq α'),
      inst ≍ inst' →
        ∀ (l : List α) (l' : List α'),
          l ≍ l' → ∀ (x : α) (x' : α'), x ≍ x' → ∀ (h : x ∈ l) (h' : x' ∈ l'), h ≍ h' → l.next x h ≍ l'.next x' h'