proposition: Fact ra_rel_fix_rec k f g : [| @ra_rec k f g |] = s_rec [|f|] [|g|].
proof: Proof. reflexivity. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec