proposition: Fact Forall2_conj X Y (R S : X -> Y -> Prop) ll mm : Forall2 (fun x y => R x y /\ S x y) ll mm <-> Forall2 R ll mm /\ Forall2 S ll mm.
proof: Proof. split. induction 1; split; constructor; tauto. intros [H1 H2]; revert H1 H2. induction 1 as [ | x ll y mm H1 H2 IH ]; intros H; auto. apply Forall2_cons_inv in H; constructor; tauto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)