proposition: Fact μ_rec_inv n x : μ_rec n x -> exists s, F (s 0) /\ s n = x /\ forall i, i < n -> G i (s i) (s (S i)).
proof: Proof. revert x; induction n as [ | n IHn ]; intros x; simpl. + exists (fun _ => x); msplit 2; auto; intros; lia. + intros (y & H1 & H2). destruct (IHn _ H1) as (s & H3 & H4 & H5). exists (fun i => if le_lt_dec (S n) i then x else s i); msplit 2; auto. * destruct (le_lt_dec (S n) (S n)); auto; lia. * intros i Hi. destruct (le_lt_dec (S n) i); destruct (le_lt_dec (S n) (S i)); auto; try lia. - replace i with n by lia. rewrite H4; auto. - apply H5; lia. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec