proposition: Lemma mapId T n (t: n.-tuple T) : map_tuple id t = t.
proof: Proof. induction n. + by rewrite (tuple0 t) mapNil. + case : t / tupleP => h t. by rewrite mapCons IHn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype seq fintype tuple)