Recv Msg comm

theorem recvMsg_comm {m1 m2 : Message P M} {s : State P M S}    (hd : m1.dest ≠ m2.dest) (h1 : m1 ∈ s.msgs) (h2 : m2 ∈ s.msgs) :    m2 ∈ (a.recvMsg m1 s).msgs ∧ m1 ∈ (a.recvMsg m2 s).msgs ∧    a.recvMsg m2 (a.recvMsg m1 s) = a.recvMsg m1 (a.recvMsg m2 s) := by  rw [State.mk.injEq]  split_ands  · grind [Algorithm.recvMsg, mem_erase_of_ne]  · grind [Algorithm.recvMsg, mem_erase_of_ne]  · have he1 (x) : (s.msgs.erase m1 + x).erase m2 = (s.msgs.erase m1).erase m2 + x := by      grind [erase_add_left_pos, mem_erase_of_ne]    have he2 (x) : (s.msgs.erase m2 + x).erase m1 = (s.msgs.erase m1).erase m2 + x := by      grind [erase_add_left_pos, mem_erase_of_ne, erase_comm]    simp [Algorithm.recvMsg, hd, hd.symm, he1, he2, add_assoc]    grind [add_comm]  · ext p    by_cases h_p1 : p = m1.dest <;> by_cases h_p2 : p = m2.dest <;>      simp [Algorithm.recvMsg, h_p1, h_p2, hd, hd.symm]