proposition: Lemma post_input_analyze_sent_packet : forall h p ms l, In p (map (fun m => mkPacket h (fst m) (snd m)) ms ++ l) -> (In (pDst p, pBody p) ms /\ h = pSrc p) \/ In p l.
proof: Proof. Proof using. intros. in_crush; destruct x; simpl in *; eauto. Qed.
imports: Verdi(Verdi)