∀ {ι : Type u_1} (a s : ι → ℕ) (l l' : List ι) (pp : l.Perm l') (nod' : l'.Nodup) (hs' : ∀ i ∈ l', s i ≠ 0),
  (∀ i ∈ l, s i ≠ 0) →
    ∀ (co' : {x | x ∈ l'}.Pairwise (Function.onFun Nat.Coprime s))
      (lco : List.Pairwise (Function.onFun Nat.Coprime s) l),
      (∀ {m' : Multiset ι} {e : ↑l = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
          {co'' : {x | x ∈ m'}.Pairwise (Function.onFun Nat.Coprime s)},
          ↑(Eq.ndrec (motive := fun m =>
                m.Nodup →
                  (∀ i ∈ m, s i ≠ 0) →
                    {x | x ∈ m}.Pairwise (Function.onFun Nat.Coprime s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
                (fun nod x co => Nat.chineseRemainderOfList a s l ⋯) e nod'' hs'' co'') =
            ↑(Nat.chineseRemainderOfList a s l lco)) →
        Eq.ndrec (motive := fun x =>
            x.Nodup →
              (∀ i ∈ x, s i ≠ 0) →
                {x_1 | x_1 ∈ x}.Pairwise (Function.onFun Nat.Coprime s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
            (fun nod x co => Nat.chineseRemainderOfList a s l ⋯) ⋯ nod' hs' co' =
          Nat.chineseRemainderOfList a s l' ⋯