(* Copied from RamifyCoq project *)

Require Import Coq.Classes.Morphisms.
Require Import Coq.Sorting.Permutation.
Require Export Coq.Relations.Relation_Definitions.
Require Import Logic.lib.Relation_ext.
Require Import Logic.lib.Equivalence_ext.
Require Export Coq.Lists.List.


Local Open Scope equiv_scope.

Section ListFun2.

Context {A B: Type}.
Context {RA: relation A}.
Context {RB: relation B}.
Context {EqRA: Equivalence RA}.
Context {EqRB: Equivalence RB}.

Instance proper_fold_left: forall (f: A -> B -> A) {Proper_f: Proper (equiv ==> equiv ==> equiv) f}, Proper (Forall2 equiv ==> equiv ==> equiv) (fold_left f).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  hnf; intros.
(* Goal: @respectful A A RA RA (@fold_left A B f x) (@fold_left A B f y) *)
  induction H; hnf; intros; simpl.
  + auto.
  + apply IHForall2.
(* Goal: @Forall2 A B P l' l *)
    apply Proper_f; auto.
Qed.

Lemma monoid_fold_left_tail: forall {f: A -> B -> A} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (e: A) a l,
  fold_left f (l ++ a :: nil) e === f (fold_left f l e) a.
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
  simpl.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' a) (f a (@fold_left A A f l' e)) *)
  pose proof (proper_fold_left f).
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
  revert e; induction l; intros; simpl.
  + reflexivity.
  + apply IHl.
Qed.

End ListFun2.

Existing Instance proper_fold_left.

Section ListFun1.

Context {A: Type}.
Context {RA: relation A}.
Context {EqRA: Equivalence RA}.

Lemma monoid_fold_left_head: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (e: A) a l,
  (forall x, f e x === x) ->
  (forall x, f x e === x) ->
  (forall x y z, f (f x y) z === f x (f y z)) ->
  fold_left f (a :: l) e === f a (fold_left f l e).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
  simpl.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' a) (f a (@fold_left A A f l' e)) *)
  pose proof (proper_fold_left f).
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f e a)) (f a (@fold_right A A f e l)) *)
  rewrite H.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
  revert a; induction l; intros; simpl.
  + symmetry; auto.
  + rewrite (IHl (f a0 a)), H, (IHl a).
(* Goal: @equiv A RA EqRA (f (f a0 a) (@fold_left A A f l e)) (f a0 (f a (@fold_left A A f l e))) *)
    rewrite H1.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
    reflexivity.
Qed.

Lemma monoid_fold_symm: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (e: A) l,
  (forall x, f e x === x) ->
  (forall x, f x e === x) ->
  (forall x y z, f (f x y) z === f x (f y z)) ->
  fold_left f l e === fold_right f e l.
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' a) (f a (@fold_left A A f l' e)) *)
  pose proof (proper_fold_left f).
(* Goal: @equiv A RA EqRA (@fold_left A A f l e) (@fold_right A A f e l) *)
  destruct l.
  + simpl.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
    reflexivity.
  + simpl.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f e a)) (f a (@fold_right A A f e l)) *)
    rewrite H.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
    revert a; induction l; intros; simpl.
(* Goal: @Forall2 A B P l' l *)
    - symmetry; auto.
    - rewrite <- H1.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f a0 a)) (f (f a0 a) (@fold_right A A f e l)) *)
      apply IHl.
Qed.

Lemma monoid_fold_left_app: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (e: A) l l',
  (forall x, f e x === x) ->
  (forall x, f x e === x) ->
  (forall x y z, f (f x y) z === f x (f y z)) ->
  fold_left f (l ++ l') e === f (fold_left f l e) (fold_left f l' e).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @equiv A RA EqRA (@fold_left A A f (@app A l l') e) (f (@fold_left A A f l e) (@fold_left A A f l' e)) *)
  rewrite fold_left_app.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  generalize (fold_left f l e) as a; clear l; intros.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' a) (f a (@fold_left A A f l' e)) *)
  pose proof @monoid_fold_left_head f _ e a l'.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' a) (f a (@fold_left A A f l' e)) *)
  simpl in H2.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' a) (f a (@fold_left A A f l' e)) *)
  pose proof (proper_fold_left f).
(* Goal: @equiv A RA EqRA (@fold_left A A f l' a) (f a (@fold_left A A f l' e)) *)
  rewrite H in H2.
(* Goal: @Forall2 A B P l' l *)
  auto.
Qed.
  
End ListFun1.

(* Above is copied from RamifyCoq project *)

Section ListFun2'.

Context {A B: Type}.
Context {RA: relation A}.
Context {RB: relation B}.

Instance proper_fold_left': forall (f: A -> B -> A) {Proper_f: Proper (RA ==> RB ==> RA) f}, Proper (Forall2 RB ==> RA ==> RA) (fold_left f).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  hnf; intros.
(* Goal: @respectful A A RA RA (@fold_left A B f x) (@fold_left A B f y) *)
  induction H; hnf; intros; simpl.
  + auto.
  + apply IHForall2.
(* Goal: @Forall2 A B P l' l *)
    apply Proper_f; auto.
Qed.

Context {EqRA: Equivalence RA}.

Lemma proper_permutation_fold_left: forall (f: A -> B -> A) {Proper_f: Proper (RA ==> eq ==> RA) f},
  (forall x1 x2 y z, x1 === x2 -> f (f x1 y) z === f (f x2 z) y) ->
  Proper (@Permutation _ ==> RA ==> RA) (fold_left f).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  hnf; intros.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  hnf; intros.
  revert x0 y0 H1.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  induction H0; intros.
  + simpl.
(* Goal: @Forall2 A B P l' l *)
    auto.
  + simpl.
    apply IHPermutation.
(* Goal: @Forall2 A B P l' l *)
    apply Proper_f; auto.
  + simpl.
    assert (RA (f (f x0 y) x) (f (f y0 x) y)) by (apply H; auto).
    revert H0; generalize (f (f x0 y) x) (f (f y0 x) y).
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
    induction l; intros.
(* Goal: @Forall2 A B P l' l *)
    - simpl; auto.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
    - simpl.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f a0 a)) (f (f a0 a) (@fold_right A A f e l)) *)
      apply IHl.
(* Goal: @Forall2 A B P l' l *)
      apply Proper_f; auto.
  + etransitivity.
    - apply IHPermutation1, H1.
    - apply IHPermutation2.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
      reflexivity.
Qed.

End ListFun2'.

Definition not_nil {A: Type} (l: list A): Prop := l <> nil.

Lemma not_nil_app_l {A: Type}: forall (l l': list A), not_nil l -> not_nil (l ++ l').
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @not_nil A (@app A l l') *)
  hnf in *.
(* Goal: forall _ : @eq (list A) (@app A l l') (@nil A), False *)
  destruct l;intros; simpl in *; congruence.
Qed.

Lemma eq_nil_dec {A: Type}: forall (l: list A), {l = nil} + {not_nil l}.
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @Forall2 A B P l' l *)
  destruct l; [left | right]; auto.
(* Goal: @not_nil A (@cons A a l) *)
  intro; congruence.
Qed.

Instance Proper_perm_not_nil {A: Type}: Proper (@Permutation A ==> iff) (@not_nil A).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  hnf; intros.
(* Goal: iff (@not_nil A x) (@not_nil A y) *)
  induction H; unfold not_nil in *.
  + reflexivity.
  + split; intros ? ?; congruence.
  + split; intros ? ?; congruence.
  + tauto.
Qed.

Definition semi_group_fold {A: Type} (default: A) (f: A -> A -> A) (l: list A): A :=
  match l with
  | nil => default
  | a :: l0 => fold_left f l0 a
  end.

Section ListFun1'.

Context {A: Type}.
Context {RA: relation A}.
Context {EqRA: Equivalence RA}.

Instance proper_semi_group_fold: forall (f: A -> A -> A) (default: A) {Proper_f: Proper (equiv ==> equiv ==> equiv) f}, Proper (Forall2 equiv ==> equiv) (semi_group_fold default f).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  hnf; intros.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f x) (@semi_group_fold A default f y) *)
  destruct H.
  + reflexivity.
  + simpl.
(* Goal: @Forall2 A B P l' l *)
    apply proper_fold_left; auto.
Qed.

Lemma semi_group_fold_app: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (default: A) l l',
  (forall x y z, f (f x y) z === f x (f y z)) ->
  not_nil l ->
  not_nil l' ->
  semi_group_fold default f (l ++ l') === f (semi_group_fold default f l) (semi_group_fold default f l').
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@app A l l')) (f (@semi_group_fold A default f l) (@semi_group_fold A default f l')) *)
  destruct l as [| a l], l' as [| a' l']; hnf in H0, H1; try congruence; clear H0 H1.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  revert a; induction l; intros.
  + simpl.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
    revert a'; induction l'; intros.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
    - simpl.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
      reflexivity.
    - specialize (IHl' (f a' a0)).
(* Goal: @equiv A RA EqRA (@fold_left A A f (@cons A a0 l') (f a a')) (f a (@fold_left A A f (@cons A a0 l') a')) *)
      simpl in *.
      rewrite <- IHl'; clear IHl'.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' (f (f a a') a0)) (@fold_left A A f l' (f a (f a' a0))) *)
      specialize (H a a' a0).
      set (b := f (f a a') a0) in H |- *.
      set (c := f a (f a' a0)) in H |- *.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' b) (@fold_left A A f l' c) *)
      clearbody b c; clear a a' a0.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
      revert b c H; induction l'; intros.
(* Goal: @Forall2 A B P l' l *)
      * auto.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
      * simpl.
(* Goal: @equiv A RA EqRA (@fold_left A A f l' (f b a)) (@fold_left A A f l' (f c a)) *)
        apply IHl'.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
        rewrite H; reflexivity.
  + exact (IHl (f a0 a)).
Qed.

Lemma semi_group_fold_concat: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (default: A) ls,
  (forall x y z, f (f x y) z === f x (f y z)) ->
  Forall not_nil ls ->
  semi_group_fold default f (concat ls) === semi_group_fold default f (map (semi_group_fold default f) ls).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
  destruct H0; [reflexivity |].
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  revert x H0; induction H1; intros.
  + simpl.
    rewrite app_nil_r.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
    reflexivity.
  + Opaque semi_group_fold.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A y (@cons A x l))) (@semi_group_fold A default f (@cons A x (@cons A y l))) *)
    simpl.
(* Goal: @Forall2 A B P l' l *)
    rewrite semi_group_fold_app; auto.
(* Goal: @Forall2 A B P l' l *)
      2: apply not_nil_app_l; auto.
    specialize (IHForall x H0).
    simpl in IHForall.
    rewrite IHForall.
    change (semi_group_fold default f x0 :: semi_group_fold default f x :: map (semi_group_fold default f) l)
      with ((semi_group_fold default f x0 :: nil) ++ semi_group_fold default f x :: map (semi_group_fold default f) l).
(* Goal: @equiv A RA EqRA (f (@semi_group_fold A default f (@cons A x (@nil A))) (@semi_group_fold A default f l)) (@semi_group_fold A default f (@app A (@cons A x (@nil A)) l')) *)
    rewrite semi_group_fold_app by (auto; intro; congruence).
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
    reflexivity.
    Transparent semi_group_fold.
Qed.

Lemma comm_semi_group_fold_perm: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (default: A) l l',
  (forall x y, f x y === f y x) ->
  (forall x y z, f (f x y) z === f x (f y z)) ->
  Permutation l l' ->
  semi_group_fold default f l === semi_group_fold default f l'.
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f l) (@semi_group_fold A default f l') *)
  induction H1.
  + reflexivity.
  + destruct (eq_nil_dec l) as [?H | ?H].
    - subst; apply Permutation_nil in H1; subst.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
      reflexivity.
    - pose proof H2.
(* Goal: @equiv A RA EqRA (@semi_group_fold A default f (@cons A x l)) (@semi_group_fold A default f (@cons A x l')) *)
      rewrite H1 in H3.
      change (x :: l) with ((x :: nil) ++ l).
      change (x :: l') with ((x :: nil) ++ l').
(* Goal: @equiv A RA EqRA (f (@semi_group_fold A default f (@cons A x (@nil A))) (@semi_group_fold A default f l)) (@semi_group_fold A default f (@app A (@cons A x (@nil A)) l')) *)
      rewrite semi_group_fold_app by (auto; intro; congruence).
(* Goal: @equiv A RA EqRA (f (@semi_group_fold A default f (@cons A x (@nil A))) (@semi_group_fold A default f l)) (@semi_group_fold A default f (@app A (@cons A x (@nil A)) l')) *)
      rewrite semi_group_fold_app by (auto; intro; congruence).
(* Goal: @equiv A RA EqRA (f (@semi_group_fold A default f (@cons A x (@nil A))) (@semi_group_fold A default f l)) (f (@semi_group_fold A default f (@cons A x (@nil A))) (@semi_group_fold A default f l')) *)
      rewrite IHPermutation.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
      reflexivity.
  + simpl.
    rewrite <- H.
(* Goal: @equiv A RA EqRA (@fold_left A A f l (f x y)) (@fold_left A A f l (f x y)) *)
    reflexivity.
  + rewrite IHPermutation1.
(* Goal: @Forall2 A B P l' l *)
    auto.
Qed.

End ListFun1'.

Lemma Forall2_impl: forall {A B: Type} (P Q: A -> B -> Prop),
  (forall a b, P a b -> Q a b) ->
  (forall (lA: list A) (lB: list B), Forall2 P lA lB -> Forall2 Q lA lB).
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @Forall2 A B Q lA lB *)
  induction H0.
  + constructor.
  + constructor.
(* Goal: @Forall2 A B P l' l *)
    - auto.
(* Goal: @Forall2 A B P l' l *)
    - auto.
Qed.

Lemma Forall2_rev: forall {A B: Type} (P: A -> B -> Prop),
  forall (lA: list A) (lB: list B), Forall2 (fun b a => P a b) lB lA -> Forall2 P lA lB.
Proof.
(* Goal: forall (A B : Type) (P : forall (_ : A) (_ : B), Prop) (lA : list A) (lB : list B) (_ : @Forall2 B A (fun (b : B) (a : A) => P a b) lB lA), @Forall2 A B P lA lB *)
  intros.
(* Goal: @Forall2 A B P lA lB *)
  induction H.
  + constructor.
  + constructor.
(* Goal: @Forall2 A B P l' l *)
    - auto.
(* Goal: @Forall2 A B P l' l *)
    - auto.
Qed.

