proposition: Lemma app_depth_r_var_S x xs n : app_depth_r (flatten (closure (x :: xs) (var (S n)))) = app_depth_r (flatten (closure xs (var n))).
proof: Proof. rewrite !flatten_var /=. have [Hn|Hn] : n < length (map flatten xs) \/ length (map flatten xs) <= n by lia. - by rewrite (nth_indep _ (var (S n)) (var n) Hn). - by rewrite !(nth_overflow _ _ Hn). Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun