proposition: Theorem map_vec_pos_equiv n (f : vec X n -> Y) : (forall p v x y, R x y -> T (f (v[x/p])) (f (v[y/p]))) -> forall v w, (forall p, R (v#>p) (w#>p)) -> T (f v) (f w).
proof: Proof. Proof using T_refl T_trans. revert f; induction n as [ | n IHn ]; intros f Hf v w H. + vec nil v; vec nil w; auto. + apply T_trans with (y := f (v[(w#>pos0)/pos0])). * rewrite <- (vec_change_same v pos0) at 1; auto. * revert H. vec split v with a; vec split w with b; intros H; simpl. apply IHn with (f := fun v => f(b##v)). - intros p q x y Hxy. apply (Hf (pos_nxt p) (b##q)); auto. - intros p; apply (H (pos_nxt p)). Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)