proposition: Lemma step_deterministic ski l1 l2 sk1 sk2 : step ski l1 sk1 -> step ski l2 sk2 -> l1 = l2 /\ sk1 = sk2.
proof: Proof. intro Hstep1. revert l2 sk2. induction Hstep1; intros l2 sk2 Hstep2; match goal with | _ : step (?s, ?k) _ _ |- _ => remember (s, k) as sk1 eqn: Heq2 end; inversion Hstep2; clear Hstep2; subst; try discriminate; match goal with | H : _ = _ |- _ => injection H; clear H; intros end; subst; repeat match goal with | H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end; subst; repeat split; congruence. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model