proposition: Lemma cfun_eodup (c : connector m) (t : (m + m).-tuple A) : cfun (ceodup c) t = teocat (cfun c (tetake t)) (cfun c (totake t)).
proof: Proof. by apply: cfun_eomerge. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple