(* stdpp/list_tactics.v *)
Ltac decompose_Forall_hyps
:=
  repeat match goal with
  | H : Forall _ [] |- _ => clear H
  | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
  | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
  | H : Forall2 _ [] [] |- _ => clear H
  | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
  | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
  | H : Forall2 _ [] ?k |- _ => apply Forall2_nil_inv_l in H
  | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H
  | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
    apply Forall2_cons_1 in H; destruct H
  | H : Forall2 _ (_ :: _) ?k |- _ =>
    let k_hd := fresh k "_hd" in let k_tl := fresh k "_tl" in
    apply Forall2_cons_inv_l in H; destruct H as (k_hd&k_tl&?&?&->);
    rename k_tl into k
  | H : Forall2 _ ?l (_ :: _) |- _ =>
    let l_hd := fresh l "_hd" in let l_tl := fresh l "_tl" in
    apply Forall2_cons_inv_r in H; destruct H as (l_hd&l_tl&?&?&->);
    rename l_tl into l
  | H : Forall2 _ (_ ++ _) ?k |- _ =>
    let k1 := fresh k "_1" in let k2 := fresh k "_2" in
    apply Forall2_app_inv_l in H; destruct H as (k1&k2&?&?&->)
  | H : Forall2 _ ?l (_ ++ _) |- _ =>
    let l1 := fresh l "_1" in let l2 := fresh l "_2" in
    apply Forall2_app_inv_r in H; destruct H as (l1&l2&?&?&->)
  | _ => progress simplify_eq/=
  | H : Forall3 _ _ (_ :: _) _ |- _ =>
    apply Forall3_cons_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
  | H : Forall2 _ (_ :: _) ?k |- _ =>
    apply Forall2_cons_inv_l in H; destruct H as (?&?&?&?&?)
  | H : Forall2 _ ?l (_ :: _) |- _ =>
    apply Forall2_cons_inv_r in H; destruct H as (?&?&?&?&?)
  | H : Forall2 _ (_ ++ _) (_ ++ _) |- _ =>
    apply Forall2_app_inv in H; [destruct H|solve_length]
  | H : Forall2 _ ?l (_ ++ _) |- _ =>
    apply Forall2_app_inv_r in H; destruct H as (?&?&?&?&?)
  | H : Forall2 _ (_ ++ _) ?k |- _ =>
    apply Forall2_app_inv_l in H; destruct H as (?&?&?&?&?)
  | H : Forall3 _ _ (_ ++ _) _ |- _ =>
    apply Forall3_app_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
  | H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
    (* to avoid some stupid loops, not fool proof *)
    unless (P x) by auto using Forall_app_2, Forall_nil_2;
    let E := fresh in
    assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E
  | H : Forall2 ?P ?l ?k |- _ =>
    match goal with
    | H1 : l !! ?i = Some ?x, H2 : k !! ?i = Some ?y |- _ =>
      unless (P x y) by done; let E := fresh in
      assert (P x y) as E by (by apply (Forall2_lookup_lr P l k i x y));
      lazy beta in E
    | H1 : l !! ?i = Some ?x |- _ =>
      try (match goal with _ : k !! i = Some _ |- _ => fail 2 end);
      destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?)
    | H2 : k !! ?i = Some ?y |- _ =>
      try (match goal with _ : l !! i = Some _ |- _ => fail 2 end);
      destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?)
    end
  | H : Forall3 ?P ?l ?l' ?k |- _ =>
    lazymatch goal with
    | H1:l !! ?i = Some ?x, H2:l' !! ?i = Some ?y, H3:k !! ?i = Some ?z |- _ =>
      unless (P x y z) by done; let E := fresh in
      assert (P x y z) as E by (by apply (Forall3_lookup_lmr P l l' k i x y z));
      lazy beta in E
    | H1 : l !! _ = Some ?x |- _ =>
      destruct (Forall3_lookup_l P _ _ _ _ _ H H1) as (?&?&?&?&?)
    | H2 : l' !! _ = Some ?y |- _ =>
      destruct (Forall3_lookup_m P _ _ _ _ _ H H2) as (?&?&?&?&?)
    | H3 : k !! _ = Some ?z |- _ =>
      destruct (Forall3_lookup_r P _ _ _ _ _ H H3) as (?&?&?&?&?)
    end
  end.