proposition: Lemma partial_to_tupleK (t : {ffun A -> T}) : [forall i in ~: s, t i == def] -> tuple_to_partial (partial_to_tuple t) = t.
proof: Proof. move/forallP => /= Hout. rewrite /tuple_to_partial /partial_to_tuple. apply/ffunP => i. rewrite ffunE. case/boolP : (i \in s) => Hi. rewrite (nth_map i) //. by rewrite nth_index // mem_enum. by rewrite index_mem mem_enum. move: (Hout i). rewrite inE Hi /= => /eqP. rewrite nth_default // leqNgt. apply: contra Hi. by rewrite size_map -mem_enum -index_mem. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner