proposition: Lemma step_star_transitive sk1 sk2 sk3 l l' : step_star sk1 l sk2 -> step_star sk2 l' sk3 -> step_star sk1 (l ++ l') sk3.
proof: Proof. intro Hss1. revert sk3 l'. induction Hss1 as [ | sk1 sk2 sk3 l Hstep Hss1 IH | sk1 sk2 sk3 t l Hstep Hss1 IH ]; intros sk3' l' Hss2; [ assumption | | ]. - apply ss_step_None with (sk2 := sk2). + exact Hstep. + apply IH; exact Hss2. - apply ss_step_Some with (sk2 := sk2). + exact Hstep. + apply IH; exact Hss2. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model