proposition: Theorem ra_ca_correct k (f : recalg k) v x : [|f|] v x <-> exists n, [f;v] -[n>> x.
proof: Proof. split; auto. Qed.
imports: Undecidability.Shared.Libs.DLW(utils finite pos vec) Undecidability.MuRec.Util(recalg recursor minimizer ra_ca)