Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  x : list A
  y : list A
  z : list A
  H : All2_fold P x y
  ============================
   (All2_fold P y z → All2_fold P x z)


DEBUG:Going to execute:
induction H in z |- *; auto; intros H'; depelim H';
            try constructor; eauto; hnf in H0; noconf ltac:(H0)