proposition: Lemma step_star_NoDup : forall s h s', step_star s h s' -> msgid_hinv (latest_label s') h.
proof: Proof. induction 1; t. split; simpl; auto. destruct H0; substs; simpl in *; unfold msgid_hinv in *; simpl in *; intuition. msgid. eapply Forall_forall in H2; eauto; lia. apply Forall_app; auto. eapply Forall_impl; [ eassumption | ]. simpl; intros; lia. msgid. eapply Forall_forall in H2; eauto; lia. eapply Forall_app; auto. eapply Forall_impl; [ eassumption | ]. simpl; intros; lia. msgid. eapply Forall_forall in H3; eauto; lia. apply Forall_app; auto. eapply Forall_impl; [ eassumption | ]. simpl; intros; lia. msgid. eapply Forall_forall in H2; eauto; lia. apply Forall_app; auto. eapply Forall_impl; [ eassumption | ]. simpl; intros; lia. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)