proposition: Lemma network_eq (net net' : orig_network) : nwState net = nwState net' -> nwPackets net = nwPackets net' -> net = net'.
proof: Proof. Proof using. intros; destruct net, net'. simpl in *. subst. auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)