proposition: Lemma ra_ca_succ_inv v n x : [ra_succ;v] -[n>> x -> n = 1 /\ x = S (vec_head v).
proof: Proof. myauto. Qed.
imports: Arith Eqdep_dec Undecidability.Shared(DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec.Util(recalg)