proposition: Lemma step_star_deterministic ski l1 l2 s1 s2 A1 A2 a1 a2 : step_star ski l1 (s1, stop A1 a1) -> step_star ski l2 (s2, stop A2 a2) -> l1 = l2 /\ s1 = s2 /\ A1 = A2 /\ JMeq a1 a2.
proof: Proof. intros Hss1 Hss2. specialize (step_star_confluent Hss1 Hss2). intros (l1' & l2' & skf & Hss1' & Hss2' & Heq). apply step_star_stop_inv in Hss1'. apply step_star_stop_inv in Hss2'. destruct Hss1' as [ Heq11 Heq12 ]. destruct Hss2' as [ Heq21 Heq22 ]. subst l1' l2' skf . do 2 rewrite cats0 in Heq. injection Heq22; clear Heq22; intros; subst. match goal with | H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end. subst. repeat split. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model