proposition: Theorem μ_rec_eq 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. split. + apply μ_rec_inv. + intros (s & H1 & H2 & H3). rewrite <- H2; clear x H2. revert s H1 H3. induction n as [ | n IHn ]; intros s H1 H2; simpl; auto. exists (s n); split; auto. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec