proposition: Fact ill_tps_vec_map_list : (forall (p : pos n) (v : vec nat n), s (rx p) v <-> v = vec_one p) -> forall v w, ill_tps_list s (map £ (vec_map_list v rx)) w <-> v = w.
proof: Proof. intros H v; rewrite map_vec_map_list. induction v as [ | p | v w Hv Hw ] using (@vec_nat_induction n); intros z. + rewrite vec_map_list_zero; simpl; tauto. + rewrite vec_map_list_one; simpl. split. * intros (a & b & H1 & H2 & H3). apply H in H2; subst; rew vec. * intros []. exists (vec_one p), vec_zero; rew vec; repeat split; auto. apply H; auto. + split. * intros Hz. apply ill_tps_perm with (1 := vec_map_list_plus _ _ _) in Hz. apply ill_tps_app in Hz. destruct Hz as (a & b & H1 & H2 & H3). apply Hv in H2. apply Hw in H3. subst; auto. * intros []. apply ill_tps_perm with (1 := Permutation_sym (vec_map_list_plus _ _ _)). apply ill_tps_app. exists v, w; repeat split; auto. - apply Hv; auto. - apply Hw; auto. Qed.
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill)