proposition: Lemma ra_ca_rec_S_inv k f g v i n x : [@ra_rec k f g; S i##v] -[n>> x -> exists y p q, n = 1+q+p /\ [ra_rec f g; i##v] -[q>> y /\ [g; i##y##v] -[p>> x.
proof: Proof. myauto; ra_inj; natSimpl. exists y', q', p'; auto. Qed.
imports: Arith Eqdep_dec Undecidability.Shared(DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec.Util(recalg)