proposition: Fact Forall2_vec_list X Y (R : X -> Y -> Prop) n v w : Forall2 R (@vec_list X n v) (vec_list w) <-> forall p, R (vec_pos v p) (vec_pos w p).
proof: Proof. revert v w; induction n as [ | n IHn ]; intros v w. + vec nil v; vec nil w; split; simpl. * intros _ p; invert pos p. * constructor. + vec split v with x; vec split w with y. simpl vec_list; rewrite Forall2_cons_inv, IHn. split. * intros (H1 & H2) p; invert pos p; auto. * intros H; split. - apply (H pos0). - intro; apply (H (pos_nxt _)). Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)