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