proposition: Fact Forall2_right_Forall X Y (P : Y -> Prop) lx ly : Forall2 (fun (_ : X) y => P y) lx ly <-> Forall P ly /\ length lx = length ly.
proof: Proof. split. intros H; split. induction H; constructor; auto. revert H; apply Forall2_length. intros (H1 & H2); revert lx H2. induction H1; intros [ | ] H2; try discriminate H2; constructor; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)