proposition: Lemma mesym_tupleE (k : nat) : 's_k = \sum_(h : k.-tuple 'I_n | tmono h) \prod_(i <- h) 'X_i.
proof: Proof. have tval_tcast T k1 k2 (eq : k1 = k2) (x : k1.-tuple T) : tval (tcast eq x) = tval x. + by rewrite /tcast; case: k2 / eq. pose t2s (t : k.-tuple 'I_n) := [set x | x \in t]. rewrite /mesym -[X in X=_]big_set -[X in _=X]big_set /=. set E := [set t2s x | x in [pred t | tmono (tval t)]]. have h: E = [set i : {set 'I_n} | #|i| == k]. apply/setP=> /= h; rewrite inE; apply/imsetP/idP=> /=. + case=> t; rewrite inE => tmono_t -> /=; rewrite /t2s. rewrite cardsE /= -[X in _==X](size_tuple t). by apply/eqP/card_uniqP/uniq_tmono. + move/eqP=> eq_sz; exists (tcast eq_sz [tuple of (enum h)]). * rewrite inE /tmono tval_tcast /=; pose I := enum 'I_n. apply/(subseq_sorted _ (s2 := [seq val i | i <- I])). exact/ltn_trans. by apply/map_subseq; rewrite /enum_mem -enumT; apply/filter_subseq. by rewrite val_enum_ord iota_ltn_sorted. * by apply/setP=> i; rewrite !(inE, memtE) tval_tcast mem_enum. rewrite -h {h}/E big_imset 1?big_set /=; last first. move=> t1 t2; rewrite !inE => tmono_t1 tmono_t2 /setP eq. by apply/val_inj/eq_tmono => // i; move: (eq i); rewrite !inE. apply/eq_big=> // i; rewrite inE 1?big_set /=. case: i => i sz_i /= tmono_i; rewrite (eq_bigl (mem i)) //=. by rewrite !mprodXE big_uniq //; apply/uniq_tmono. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg