proposition: Lemma packet_eta : forall p : packet, {| pSrc := pSrc p; pDst := pDst p; pBody := pBody p |} = p.
proof: Proof. Proof using. destruct p; auto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)