Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  n : nat
  Γ : list A
  Γ' : list A
  d : A
  ============================
   (All2_fold P Γ Γ'
    → nth_error Γ n = Some d
      → ∑ d' : A,
          nth_error Γ' n = Some d'
          × (let Γs := skipn (S n) Γ in
             let Γs' := skipn (S n) Γ' in All2_fold P Γs Γs' × P Γs Γs' d d'))


DEBUG:Going to execute:
induction n in Γ, Γ', d |- *; destruct Γ; intros Hrel H