proposition: Lemma boundS m n : L_facts.bound (S m) (var (S n)) -> L_facts.bound m (var n).
proof: Proof. move=> /term_facts.boundE ?. constructor. lia. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun