proposition: Lemma ra_bs_from_c k (f : recalg k) c v x : [f ; v ; 0 ; c] ▹ x -> [ f; v ] ▹ x.
proof: Proof. remember 0 as min. induction 1; subst; eauto using ra_bs. econstructor. + intros; eapply H1; lia. + auto. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq)