proposition: Lemma dio_repr_at_exst R a n m p : dio_repr_at R a n p -> m = n+1 -> dio_repr_at (fun ν => exists n, R n·ν) a m p.
proof: Proof. intros [ l r F0 F1 F2 F3 F4 ] ?; subst m. exists (map (dc_dec (a+n)) l) r. + rewrite map_length; auto. + intros x c'; rewrite in_map_iff. intros (c & E & Hc) H; subst. apply dc_vars_dec in H. destruct H as [ | H ]; subst; simpl; try lia. apply F1 in H; simpl in *; auto; lia. + lia. + intros f. destruct (F3 (fun x => match x with 0 => 0 | S x => f x end)) as (g & Hg). exists (fun x => if eq_nat_dec x (a+n) then 0 else g x). rewrite Forall_map. apply Forall_impl with (2 := Hg). intros c Hc; rewrite dc_eval_dec; apply dc_eval_ext; auto. * intros x Hx. destruct (eq_nat_dec x (a+n)); subst; auto. apply F1 in Hx; auto; lia. * intros [ | x ]; auto. destruct (eq_nat_dec (a+n) (a+n)); tauto. + intros f; split. * intros (u & Hu). apply F4 in Hu. destruct Hu as (g & H1 & H2). exists (fun x => if eq_nat_dec x (a+n) then u else g x); simpl; split. - rewrite Forall_map. apply Forall_impl with (2 := H1). intros c Hc; rewrite dc_eval_dec; apply dc_eval_ext; auto. ++ intros x Hx. destruct (eq_nat_dec x (a+n)); auto. subst x; apply F1 in Hx; auto; lia. ++ intros [ | x ]; auto. destruct (eq_nat_dec (a+n) (a+n)); tauto. - destruct (eq_nat_dec r (a+n)); auto. subst; lia. * intros (g & H1 & H2). exists (g (a+n)); rewrite F4. exists g; split; auto. revert H1; do 2 rewrite Forall_forall. intros H c Hc. apply in_map with (f := dc_dec _), H in Hc. revert Hc; rewrite dc_eval_dec; apply dc_eval_ext; auto. intros []; simpl; auto. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)