proposition: Lemma app_depth_r_lam xs s : app_depth_r (flatten (closure xs (lam s))) = app_depth_r (flatten (closure (closure [] (var 0) :: xs) s)).
proof: Proof. by rewrite /= app_depth_r_subst_many_repeat. 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