proposition: Lemma mapCons {n A B} (f: A -> B) b (p: n.-tuple A) : map_tuple f [tuple of b :: p] = [tuple of f b :: map_tuple f p].
proof: Proof. by apply: eq_from_tnth=> i; rewrite !(tnth_nth (f b)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype seq fintype tuple)