proposition: Lemma Rmessages_map : forall A f1 f2 (ms : list A), (forall x, N.ICExec.msg_key (f1 x) = N.CExec.msg_key (f2 x)) -> (forall x, N.ICExec.msg_val (f1 x) = N.CExec.msg_val (f2 x)) -> (forall x, RUpdate R (N.ICExec.msg_update (f1 x)) (N.CExec.msg_update (f2 x))) -> (forall x, N.ICExec.msg_receiver (f1 x) = N.CExec.msg_receiver (f2 x)) -> Rmessages (map f1 ms) (map f2 ms).
proof: Proof. induction ms; simpl; intuition. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)