proposition: Lemma mm2_instr_at_state_bound {mm2i p} : mm2_instr_at mm2i p mm -> S p < state_bound /\ instr_state mm2i < state_bound.
proof: Proof. rewrite /state_bound. move=> [?] [?] [-> <-]. rewrite !app_length !map_app !list_sum_app /=. split; lia. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun