proposition: Lemma step_det: forall s1 s2 l, step s1 l s2 -> msgid_inv s1 -> forall s3, step s1 l s3 -> s2 = s3.
proof: Proof. destruct 1; (inversion 2; substs; try match goal with | [ H' : msgid_inv _, H : _ ++ _ = _ ++ _ |- _ ] => destruct H'; simpl in *; symmetry in H; eapply NoDup_map_middle in H; [ | eauto | eauto ]; intuition subst end; repeat match goal with | [ H : _ = _ |- _ ] => rewrite H end; repeat (eapply re_override; [ solve [ eauto ] | inversion 1; congruence ] || f_equal)). Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)