proposition: Lemma ra_ca_cst_inv i v n x : [ra_cst i;v] -[n>> x -> n = 1 /\ x = i.
proof: Proof. inversion_clear 1; auto. Qed.
imports: Arith Eqdep_dec Undecidability.Shared(DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec.Util(recalg)