proposition: Lemma step_msgid_inv: forall s1 s2 l, step s1 l s2 -> msgid_inv s1 -> msgid_inv s2.
proof: Proof. destruct 1; substs; unfold msgid_inv; simpl; intuition. - msgid. destruct (nid_eq_dec (msg_sender x) (msg_receiver x)); try discriminate. eapply Forall_forall in H2; eauto. autorewrite with core in *; simpl in *; intuition; try lia. - apply Forall_app; auto. eapply Forall_impl; [ eassumption | ]. simpl; intros. destruct (nid_eq_dec n (msg_sender x)); subst; autorewrite with core in *; simpl in *; auto; lia. apply Forall_map; simpl. autorewrite with core; simpl. apply Forall_forall; auto. - eapply Forall_impl; [ eassumption | ]. simpl; intros. destruct (nid_eq_dec n (msg_sender x)); subst; autorewrite with core in *; simpl in *; auto; lia. - autorewrite with core in *; simpl in *. apply NoDup_app_bwd in H2; intuition. inversion_clear H2. eapply NoDup_app; eauto. simpl in *. intuition eauto. - apply Forall_app_bwd in H3; intuition. inversion_clear H4. eapply Forall_app; eauto. eapply Forall_impl; [ eassumption | ]. simpl; intros. destruct (nid_eq_dec n (msg_sender x)); subst; autorewrite with core in *; simpl in *; auto; lia. eapply Forall_impl; [ eassumption | ]. simpl; intros. destruct (nid_eq_dec n (msg_sender x)); subst; autorewrite with core in *; simpl in *; auto; lia. - eapply Forall_impl; [ eassumption | ]. simpl; intros. destruct (nid_eq_dec n (msg_sender x)); subst; autorewrite with core in *; simpl in *; auto; lia. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)