proposition: Lemma cfun_dup (c : connector m) (t : (m + m).-tuple A) : cfun (cdup c) t = [tuple of cfun c (ttake t) ++ cfun c (tdrop t)].
proof: Proof. by apply: cfun_merge. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple