proposition: Lemma ra_bs_mono min k (f : recalg k) v c1 x : [f ; v ; min ; c1 ] ▹ x -> forall c2, c1 <= c2 -> [f ; v ; min; c2] ▹ x.
proof: Proof. induction 1; intros; try (destruct c2;[ lia | ]). - econstructor. - econstructor. - econstructor. - econstructor. - destruct c2; try lia. econstructor. + intros. eapply H0. lia. + eapply IHra_bs_c. lia. - econstructor. eapply IHra_bs_c. lia. - econstructor. + eapply IHra_bs_c1. lia. + eapply IHra_bs_c2. lia. - econstructor. + lia. + intros. eapply H1; lia. + eapply IHra_bs_c. lia. 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)