proposition: Lemma eval_to_sss_out_code n i (P : list (mm_instr (pos n))) c (v : vec nat n) c' v' : eval (i, P) (c, v) (c', v') -> subcode.out_code (fst (c', v')) (i, P).
proof: Proof. generalize (i, P) as iP. generalize (c, v) as cv. generalize (c', v') as c'v'. clear. induction 1 as [ i P c v | i P c v j b c' v' H1 H2 H | i P c v j c1 c2 c' v' l H1 H2 H3 H | i P c v j c1 c2 c' v' H1 H2 H3 H ]; cbn in *. all: lia. Qed.
imports: Coq(List Lia) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) Undecidability.MinskyMachines.MM