proposition: Lemma update_no_self_message: forall p h s m, step_star (init p) h s /\ In m (messages s) -> not (sender_node (msg_update m) = msg_receiver m).
proof: Proof. intros. destruct H as [H1 H2]. assert (A1 := update_sender_eq_msg_sender p h s m). depremise A1. split; assumption. assert (A2 := no_self_message p h s m). depremise A2. split; assumption. rewrite <- A1 in A2. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)