proposition: Fact mm_sss_env_total ii s : { t | ii // s -1> t }.
proof: Proof. destruct s as (i,v). destruct ii as [ x | x j ]; [ | case_eq (v⇢x); [ | intros k ]; intros E ]. * exists (1+i,v⦃x⇠S(v⇢x)⦄); constructor. * exists (j,v); constructor; auto. * exists (1+i,v⦃x⇠k⦄); constructor; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode sss) Undecidability.MinskyMachines.MMenv(env)