proposition: Lemma no_self_message: forall p h s m, step_star (init p) h s /\ In m (messages s) -> (not (msg_sender m = msg_receiver m)).
proof: Proof. intros. open_conjs. remember (init p) as s0 eqn: Hi. induction H. subst s. simpl in H0. contradiction. depremise IHstep_star. assumption. inversion H1. rewrite <- H5 in H0. simpl in H0. apply in_app_iff in H0. destruct H0 as [H0 | H0]. depremise IHstep_star. rewrite <- H3. simpl. assumption. assumption. apply in_map_iff in H0. destruct H0 as [n' [N1 N2]]. subst m. simpl in *. apply filter_In in N2. destruct N2 as [N2 N3]. destruct (nid_eq_dec n n'). inversion N3. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. depremise IHstep_star. rewrite <- H5 in H0. assumption. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. depremise IHstep_star. rewrite <- H6 in H0. simpl in H0. apply in_app_iff in H0. destruct H0 as [H0 | H0]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. depremise IHstep_star. rewrite <- H5 in H0. simpl in H0. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)