proposition: Lemma eval_to_sss_out_code n i (P : list (bsm_instr n)) c (v : vec (list bool) n) c' v' : eval n (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 IH | i P c v j c1 c2 c' v' l H1 H2 H3 H IH | i P c v j c1 c2 c' v' l H1 H2 H3 H IH | i P c v j c1 c2 c' v' H1 H2 H3 H IH]; cbn in *. all: lia. Qed.
imports: Undecidability.StackMachines.BSM List Bool Lia Nat Undecidability.Shared.Libs.DLW(list_bool pos vec sss)