proposition: Lemma nfun_dup (n : network m) (t : (m + m).-tuple A) : nfun (ndup n) t = [tuple of nfun n (ttake t) ++ nfun n (tdrop t)].
proof: Proof. by apply: nfun_merge. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple