proposition: Lemma nw_nw_distinct_pairs_and_elim : forall xs a b ys l, l = xs ++ a :: ys -> In b (xs ++ ys) -> distinct_pairs_and network_network_invariant l -> network_network_invariant a b.
proof: Proof. Proof using. induction xs; intros; subst; simpl in *; intuition eauto; subst; eauto. apply network_network_invariant_sym. eauto. Qed.
imports: Verdi(Verdi)