proposition: Theorem eval_iff n i (P : list (bsm_instr n)) c (v : vec (list bool) n) c' v' : eval n (i, P) (c, v) (c', v') <-> sss_output (@bsm_sss _) (i,P) (c, v) (c', v').
proof: Proof. split. - intros H. split. + now eapply eval_to_sss_compute. + eapply eval_to_sss_out_code. eassumption. - intros H. now eapply sss_output_to_eval. Qed.
imports: Undecidability.StackMachines.BSM List Bool Lia Nat Undecidability.Shared.Libs.DLW(list_bool pos vec sss)