proposition: Fact ra_proj_inj k (p q : pos k) : ra_proj p = ra_proj q -> p = q.
proof: Proof. inj. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec