proposition: Lemma nfun_eodup (n : network m) (t : (m + m).-tuple A) : nfun (neodup n) t = teocat (nfun n (tetake t)) (nfun n (totake t)).
proof: Proof. elim: n t => /= [t|c n IH t]; first by rewrite -eocat_tetake_totake. by rewrite IH !cfun_eodup tetakeK totakeK. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple