proposition: Fact vec_one_nxt n p : @vec_one (S n) (pos_nxt p) = 0##vec_one p.
proof: Proof. apply vec_pos_ext. unfold vec_one. intros q; rewrite vec_pos_set. pos_inv q. + simpl; auto. + rewrite <- vec_pos_tail. simpl vec_tail. rewrite vec_pos_set. destruct (pos_eq_dec p q) as [ | C ]. * subst. destruct (pos_eq_dec (pos_nxt q) (pos_nxt q)) as [ | [] ]; auto. * destruct (pos_eq_dec (pos_nxt p) (pos_nxt q)) as [ | ]; auto. destruct C; apply pos_nxt_inj; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)