proposition: Fact vec_app_split u : let (v,w) := vec_split u in vec_app v w = u.
proof: Proof. case_eq (vec_split u); intros v w; unfold vec_split, vec_app; intros H. injection H; clear H; intros Hw Hv. apply vec_pos_ext; unfold vec_app; simpl. intros p; rewrite vec_pos_set. case_eq (pos_both n m p); intros q Hq. + rewrite <- Hv, vec_pos_set; f_equal. apply f_equal with (f := @pos_lr _ _) in Hq. simpl in Hq; rewrite <- Hq; apply pos_lr_both. + rewrite <- Hw, vec_pos_set; f_equal. apply f_equal with (f := @pos_lr _ _) in Hq. simpl in Hq; rewrite <- Hq; apply pos_lr_both. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)