lemma eq_of_kth_eq [deceqA : decidable_eq A]
      : ∀ {l1 l2 : list A} (Pleq : length l1 = length l2),
          (∀ (k : nat) (Plt1 : k < length l1) (Plt2 : k < length l2), kth k l1 Plt1 = kth k l2 Plt2) → l1 = l2
| []       []       h₁ h₂ := rfl
| (a₁::l₁) []       h₁ h₂ := by contradiction
| []       (a₂::l₂) h₁ h₂ := by contradiction
| (a₁::l₁) (a₂::l₂) h₁ h₂ :=
  have ih₁ : length l₁ = length l₂, by injection h₁; eassumption,
  have ih₂ : ∀ (k : nat) (plt₁ : k < length l₁) (plt₂ : k < length l₂), kth k l₁ plt₁ = kth k l₂ plt₂,
    begin
      intro k plt₁ plt₂,
      have splt₁ : succ k < length l₁ + 1, from succ_le_succ plt₁,
      have splt₂ : succ k < length l₂ + 1, from succ_le_succ plt₂,
      have keq   : kth (succ k) (a₁::l₁) splt₁ = kth (succ k) (a₂::l₂) splt₂, from h₂ (succ k) splt₁ splt₂,
      rewrite *kth_succ_of_cons at keq,
      exact keq
    end,
  assert ih  : l₁ = l₂, from eq_of_kth_eq ih₁ ih₂,
  assert k₁  : a₁ = a₂,
    begin
      have lt₁ : 0 < length (a₁::l₁), from !zero_lt_succ,
      have lt₂ : 0 < length (a₂::l₂), from !zero_lt_succ,
      have e₁  : kth 0 (a₁::l₁) lt₁ = kth 0 (a₂::l₂) lt₂, from h₂ 0 lt₁ lt₂,
      rewrite *kth_zero_of_cons at e₁,
      assumption
    end,
  by subst l₁; subst a₁