proposition: Lemma nfun_merge (n1 n2 : network m) (t : (m + m).-tuple A) : size n1 = size n2 -> nfun (nmerge n1 n2) t = [tuple of nfun n1 (ttake t) ++ nfun n2 (tdrop t)].
proof: Proof. elim: n1 n2 t => /= [[]//= t sn1Esn2|c1 n1 IH [|c2 n2]// t [sn1Esn2]]. by apply: cat_ttake_tdrop. by rewrite /= IH // !cfun_merge ttakeK tdropK. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple