proposition: Lemma cfun_merge m1 m2 (c1 : connector m1) (c2 : connector m2) (t : (m1 + m2).-tuple A) : cfun (cmerge c1 c2) t = [tuple of cfun c1 (ttake t) ++ cfun c2 (tdrop t)].
proof: Proof. apply: eq_from_tnth => i. pose a := tnth t i. rewrite /= !(tnth_nth a) /= ?nth_cat !(nth_map i) /=; last 2 first. - by rewrite -fintype.enumT -enum_ord size_enum_ord. - by rewrite -enum_ord size_enum_ord. set u := nth i _ _; have -> : u = i. by apply/val_eqP; rewrite /= /u -fintype.enumT -enum_ord /= nth_enum_ord. rewrite {u}size_map -enum_ord size_enum_ord. rewrite /= !(tnth_nth a) !ffunE /=; case: splitP => /= [j iE|k iE]; rewrite iE. rewrite (nth_map j) /=; last by rewrite size_enum_ord. set u := nth j _ _; have -> : u = j. by apply/val_eqP; rewrite /= /u nth_enum_ord. by rewrite !(tnth_nth a) /= ttakeE !nth_take. rewrite leq_add2l addKn (nth_map k) /=; last first. by rewrite -enum_ord size_enum_ord. set u := nth k _ _; have -> : u = k. by apply/val_eqP; rewrite /= /u -enum_ord nth_enum_ord. by rewrite !(tnth_nth a) /= tdropE !nth_drop. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple